NYLL
Module

Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.lean

Nyll.AlgebraicCurves.Places.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
9 declarations indexed from sourceView source ↗

Module documentation

Place ramification Index forget Constants eq one of adjoin range eq top

Imports4
Imported by2

Declarations

theorem

ord_nonneg_of_mem

L35 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.ord_nonneg_of_mem
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
Lean source · statement
theorem ord_nonneg_of_mem {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
    {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L51 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.mem_of_ord_nonneg
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
Lean source · statement
theorem mem_of_ord_nonneg {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
    {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) : f ∈ v.toValuationSubring
theorem

exists_ord_eq_one

L59 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.exists_ord_eq_one
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
Lean source · statement
theorem exists_ord_eq_one {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) :
    ∃ π : F, v.ord π = 1
theorem

isScalarTower_valuationSubring

L71 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.isScalarTower_valuationSubring
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
section FiniteLayer
variable {K F L : Type*} [Field K] [Field F] [Field L]
  [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L]
omit [FiniteDimensional F L] [Algebra.IsSeparable F L] in
Lean source · statement
theorem isScalarTower_valuationSubring (v : Place K F) :
    IsScalarTower K v.toValuationSubring L
theorem

differentIdeal_integralClosureAt_eq_top

L78 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.differentIdeal_integralClosureAt_eq_top
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
section FiniteLayer
variable {K F L : Type*} [Field K] [Field F] [Field L]
  [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L]
Lean source · statement
theorem differentIdeal_integralClosureAt_eq_top
    {α : L} (hα : IsIntegral K α) (hsep : (minpoly K α).Separable)
    (htop : Algebra.adjoin F ({α} : Set L) = ⊤) (v : Place K F) :
    differentIdeal v.toValuationSubring (Place.integralClosureAt L v) = ⊤
theorem

ramificationIndex_eq_one_finiteLayer

L135 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.ramificationIndex_eq_one_finiteLayer
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
section FiniteLayer
variable {K F L : Type*} [Field K] [Field F] [Field L]
  [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L]
Lean source · statement
theorem ramificationIndex_eq_one_finiteLayer
    {α : L} (hα : IsIntegral K α) (hsep : (minpoly K α).Separable)
    (htop : Algebra.adjoin F ({α} : Set L) = ⊤) (W : Place K L) :
    W.ramificationIndex F = 1
theorem

exists_finset_mem_adjoin

L171 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.exists_finset_mem_adjoin
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
section Reduction
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem exists_finset_mem_adjoin {t : F'} (ht : t ∈ Algebra.adjoin F (Set.range (algebraMap K'
  F'))) :
    ∃ S : Finset K', t ∈ Algebra.adjoin F ((algebraMap K' F') '' (S : Set K'))
theorem

main

L193 ↗
AlgebraicCurves.Places.Proofs.Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top.S28CF.main
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S28CF
section Reduction
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem main [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (W : Place K' F') :
    (W.forgetConstants (K := K)).ramificationIndex F = 1
theorem

ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top

L303 ↗
AlgebraicCurve.Place.ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ramificationIndex_forgetConstants_eq_one_of_adjoin_range_eq_top
    {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
    [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (W : AlgebraicCurve.Place K' F') :
    (W.forgetConstants (K := K)).ramificationIndex F = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.