Module

Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.lean

Nyll.AlgebraicCurves.Places.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois

63 declarations indexed from sourceView source ↗

Module documentation

Place ord restrict Along eq nat Card alg Hom of is Galois

Imports12

Imported by2

theorem

mem_of_ord_nonneg

L46 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.mem_of_ord_nonneg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_of_ord_nonneg (w : Place K F) {f : F} (hf : f ≠ 0) (h : 0 ≤ w.ord f) :
    f ∈ w.toValuationSubring

theorem

mem_of_ord_sub_pos

L54 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.mem_of_ord_sub_pos

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_of_ord_sub_pos (w : Place K F) {f : F} {c : K}
    (h : 0 < w.ord (f - algebraMap K F c)) : f ∈ w.toValuationSubring

theorem

ord_eq_one_of_valuation_eq

L63 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.ord_eq_one_of_valuation_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ord_eq_one_of_valuation_eq (w : Place K F) {v' : Valuation F ℤᵐ⁰}
    (hv' : v'.valuationSubring = w.toValuationSubring) {x : F} (hx : v' x = exp (-1 : ℤ)) :
    w.ord x = 1

instance

instIsPrincipalIdealRingAdjoinSingleton

L96 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.instIsPrincipalIdealRingAdjoinSingleton

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

instance instIsPrincipalIdealRingAdjoinSingleton (t : F) :
    IsPrincipalIdealRing (Algebra.adjoin K ({t} : Set F))

def

linGen

L112 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.linGen

Documentation

The difference of the adjoined generator and a base-field constant in the polynomial subalgebra.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

def linGen (t : F) (c : K) : Algebra.adjoin K ({t} : Set F)

theorem

coe_linGen

L115 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.coe_linGen

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem coe_linGen (t : F) (c : K) :
    ((linGen t c : Algebra.adjoin K ({t} : Set F)) : F) = t - algebraMap K F c

theorem

linGen_ne_zero

L124 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.linGen_ne_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
include htr in

Lean source · statement

theorem linGen_ne_zero (c : K) : linGen t c ≠ 0

def

polyEquiv

L131 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.polyEquiv

Documentation

The polynomial algebra equivalence furnished by a transcendental generator.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)

Lean source · statement

def polyEquiv : Polynomial K ≃ₐ[K] Algebra.adjoin K ({t} : Set F)

theorem

polyEquiv_X_sub_C

L135 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.polyEquiv_X_sub_C

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)

Lean source · statement

theorem polyEquiv_X_sub_C (c : K) :
    polyEquiv t htr (Polynomial.X - Polynomial.C c) = linGen t c

theorem

prime_linGen

L141 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.prime_linGen

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
include htr in

Lean source · statement

theorem prime_linGen (c : K) : Prime (linGen t c)

def

linPrime

L146 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.linPrime

Documentation

The height-one prime generated by the difference of the generator and a constant.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)

Lean source · statement

def linPrime (c : K) : HeightOneSpectrum (Algebra.adjoin K ({t} : Set F))

def

basePlace

L155 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.basePlace

Documentation

The place on the simple transcendental subfield corresponding to a base-field constant.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
open scoped IntermediateField.algebraAdjoinAdjoin

Lean source · statement

def basePlace (c : K) : Place K (IntermediateField.adjoin K ({t} : Set F))

theorem

algebraMap_linGen

L158 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.algebraMap_linGen

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
open scoped IntermediateField.algebraAdjoinAdjoin

Lean source · statement

theorem algebraMap_linGen (c : K) :
    algebraMap (Algebra.adjoin K ({t} : Set F)) (IntermediateField.adjoin K ({t} : Set F))
        (linGen t c) =
      IntermediateField.AdjoinSimple.gen K t - algebraMap K _ c

theorem

ord_basePlace

L166 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.ord_basePlace

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
open scoped IntermediateField.algebraAdjoinAdjoin

Lean source · statement

theorem ord_basePlace (c : K) :
    (basePlace t htr c).ord (IntermediateField.AdjoinSimple.gen K t - algebraMap K _ c) = 1

theorem

forall_algebraMap_mem

L174 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.forall_algebraMap_mem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
open scoped IntermediateField.algebraAdjoinAdjoin

Lean source · statement

theorem forall_algebraMap_mem (v : Place K (IntermediateField.adjoin K ({t} : Set F)))
    (ht : IntermediateField.AdjoinSimple.gen K t ∈ v.toValuationSubring)
    (r : Algebra.adjoin K ({t} : Set F)) :
    algebraMap (Algebra.adjoin K ({t} : Set F)) (IntermediateField.adjoin K ({t} : Set F)) r ∈
      v.toValuationSubring

theorem

eq_basePlace_of_ord_pos

L191 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.eq_basePlace_of_ord_pos

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
open scoped IntermediateField.algebraAdjoinAdjoin
include htr in

Lean source · statement

theorem eq_basePlace_of_ord_pos (v : Place K (IntermediateField.adjoin K ({t} : Set F))) (c : K)
    (hv : 0 < v.ord (IntermediateField.AdjoinSimple.gen K t - algebraMap K _ c)) :
    v = basePlace t htr c

theorem

restrict_eq_basePlace

L212 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.restrict_eq_basePlace

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Engine
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section Transcendental
variable (t : F) (htr : Transcendental K t)
open scoped IntermediateField.algebraAdjoinAdjoin
include htr in

Lean source · statement

theorem restrict_eq_basePlace [Algebra.IsIntegral (IntermediateField.adjoin K ({t} : Set F)) F]
    (w : Place K F) (c : K) (hw : 0 < w.ord (t - algebraMap K F c)) :
    w.restrict (IntermediateField.adjoin K ({t} : Set F)) = basePlace t htr c ∧
    (w.restrict (IntermediateField.adjoin K ({t} : Set F))).ord
      (IntermediateField.AdjoinSimple.gen K t - algebraMap K _ c) = 1

def

adjoinEquivAlong

L247 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.adjoinEquivAlong

Documentation

The equivalence between simple intermediate fields induced by a field embedding.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Along
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (ι : F →ₐ[K] M) (y : F)

Lean source · statement

def adjoinEquivAlong :
    IntermediateField.adjoin K ({y} : Set F) ≃ₐ[K] IntermediateField.adjoin K ({ι y} : Set M)

theorem

coe_adjoinEquivAlong

L252 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.coe_adjoinEquivAlong

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Along
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (ι : F →ₐ[K] M) (y : F)

Lean source · statement

theorem coe_adjoinEquivAlong (r : IntermediateField.adjoin K ({y} : Set F)) :
    ((adjoinEquivAlong ι y r : IntermediateField.adjoin K ({ι y} : Set M)) : M) = ι r

theorem

finiteAlong_of_finiteDimensional_adjoin

L255 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.finiteAlong_of_finiteDimensional_adjoin

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Along
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (ι : F →ₐ[K] M) (y : F)

Lean source · statement

theorem finiteAlong_of_finiteDimensional_adjoin
    [h : FiniteDimensional (IntermediateField.adjoin K ({ι y} : Set M)) M] :
    FiniteAlong K ι

theorem

separableAlong_of_isSeparable_adjoin

L280 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.separableAlong_of_isSeparable_adjoin

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Along
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (ι : F →ₐ[K] M) (y : F)

Lean source · statement

theorem separableAlong_of_isSeparable_adjoin
    [Algebra.IsSeparable (IntermediateField.adjoin K ({ι y} : Set M)) M] :
    SeparableAlong K ι

theorem

isIntegral_of_finiteAlong

L302 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.isIntegral_of_finiteAlong

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Along
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (ι : F →ₐ[K] M) (y : F)

Lean source · statement

theorem isIntegral_of_finiteAlong (hfin : FiniteAlong K ι) : ι.toRingHom.IsIntegral

theorem

normalAlong_of_normal_adjoin

L308 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.normalAlong_of_normal_adjoin

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Along
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (ι : F →ₐ[K] M) (y : F)

Lean source · statement

theorem normalAlong_of_normal_adjoin
    [Normal (IntermediateField.adjoin K ({ι y} : Set M)) M] :
    @Normal F M _ _ (algebraAlong ι)

def

toSemilinear

L348 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.toSemilinear

Documentation

The homomorphism viewing intermediate-field automorphisms as semilinear base-field automorphisms.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]

Lean source · full declaration

def toSemilinear : (M ≃ₐ[E] M) →* SemilinearAut K M where
  toFun σ := SemilinearAut.ofAlgAut (σ.restrictScalars K)
  map_one' := by ext <;> rfl
  map_mul' _ _ := by ext <;> rfl

def

placeAction

L354 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.placeAction

Documentation

The induced action of intermediate-field automorphisms on places.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]

Lean source · statement

def placeAction : MulAction (M ≃ₐ[E] M) (Place K M)

theorem

smul_place_def

L361 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.smul_place_def

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}

Lean source · statement

theorem smul_place_def (σ : M ≃ₐ[E] M) (W : Place K M) :
    σ • W = SemilinearAut.ofAlgAut (σ.restrictScalars K) • W

theorem

mem_smul_place_iff

L364 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.mem_smul_place_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}

Lean source · statement

theorem mem_smul_place_iff (σ : M ≃ₐ[E] M) (W : Place K M) (y : M) :
    y ∈ (σ • W).toValuationSubring ↔ σ.symm y ∈ W.toValuationSubring

theorem

ord_smul_apply

L370 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.ord_smul_apply

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}

Lean source · statement

theorem ord_smul_apply (σ : M ≃ₐ[E] M) (W : Place K M) (y : M) : (σ • W).ord (σ y) = W.ord y

theorem

ord_apply_of_smul_eq

L373 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.ord_apply_of_smul_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}

Lean source · statement

theorem ord_apply_of_smul_eq {σ : M ≃ₐ[E] M} {W : Place K M} (h : σ • W = W) (y : M) :
    W.ord (σ y) = W.ord y

theorem

mem_fiberOver_iff_mem_orbit

L380 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.mem_fiberOver_iff_mem_orbit

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}
variable [FiniteDimensional E M] [IsGalois E M]

Lean source · statement

theorem mem_fiberOver_iff_mem_orbit (P W : Place K M) :
    W ∈ (P.restrict E).fiberOver M ↔ W ∈ MulAction.orbit (M ≃ₐ[E] M) P

theorem

card_stabilizer_mul_card_fiberOver

L390 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.card_stabilizer_mul_card_fiberOver

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}
variable [FiniteDimensional E M] [IsGalois E M]

Lean source · statement

theorem card_stabilizer_mul_card_fiberOver (P : Place K M) :
    Nat.card (MulAction.stabilizer (M ≃ₐ[E] M) P) * ((P.restrict E).fiberOver M).card =
      Module.finrank E M

theorem

inertiaDeg_eq_one_of_deg_eq_one

L403 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.inertiaDeg_eq_one_of_deg_eq_one

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}
variable [FiniteDimensional E M] [IsGalois E M]
omit [FiniteDimensional E M] [IsGalois E M] in

Lean source · statement

theorem inertiaDeg_eq_one_of_deg_eq_one {F' : Type*} [Field F'] [Algebra K F'] [Algebra F' M]
    [IsScalarTower K F' M] [Algebra.IsIntegral F' M] (W : Place K M) (hW : W.deg = 1) :
    W.inertiaDeg F' = 1

theorem

card_stabilizer_eq

L410 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.card_stabilizer_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Galois
variable (K E M : Type*) [Field K] [Field E] [Field M]
  [Algebra K E] [Algebra K M] [Algebra E M] [IsScalarTower K E M]
attribute [local instance] placeAction
variable {K E M}
variable [FiniteDimensional E M] [IsGalois E M]

Lean source · statement

theorem card_stabilizer_eq (P : Place K M) (hdeg : P.deg = 1) :
    Nat.card (MulAction.stabilizer (M ≃ₐ[E] M) P) = P.ramificationIndex E

def

adjoinEquivNorm

L431 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.adjoinEquivNorm

Documentation

The simple-field equivalence induced by an embedding sending the selected generator to its target.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

def adjoinEquivNorm (ψ : F →ₐ[K] M) (hψ : ψ x = t) : K⟮x⟯ ≃ₐ[K] K⟮t⟯

theorem

coe_adjoinEquivNorm

L434 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.coe_adjoinEquivNorm

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

theorem coe_adjoinEquivNorm (ψ : F →ₐ[K] M) (hψ : ψ x = t) (r : K⟮x⟯) :
    ((adjoinEquivNorm x t ψ hψ r : K⟮t⟯) : M) = ψ r

def

baseHom

L438 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.baseHom

Documentation

The map back to the source field obtained from the inverse simple-field equivalence.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

def baseHom (ψ : F →ₐ[K] M) (hψ : ψ x = t) : K⟮t⟯ →+* F

theorem

psi_baseHom

L441 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.psi_baseHom

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

theorem psi_baseHom (ψ : F →ₐ[K] M) (hψ : ψ x = t) (r : K⟮t⟯) : ψ (baseHom x t ψ hψ r) = r

theorem

baseHom_mem

L445 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.baseHom_mem

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

theorem baseHom_mem (ψ : F →ₐ[K] M) (hψ : ψ x = t) (r : K⟮t⟯) : baseHom x t ψ hψ r ∈ K⟮x⟯

theorem

apply_eq_of_mem_adjoin

L448 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.apply_eq_of_mem_adjoin

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

theorem apply_eq_of_mem_adjoin (ψ ψ' : F →ₐ[K] M) (hψ : ψ x = t) (hψ' : ψ' x = t) {f : F}
    (hf : f ∈ K⟮x⟯) : ψ f = ψ' f

theorem

psi'_baseHom

L458 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.psi'_baseHom

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

theorem psi'_baseHom (ψ ψ' : F →ₐ[K] M) (hψ : ψ x = t) (hψ' : ψ' x = t) (r : K⟮t⟯) :
    ψ' (baseHom x t ψ hψ r) = r

theorem

exists_algEquiv_comp_eq

L463 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.exists_algEquiv_comp_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)

Lean source · statement

theorem exists_algEquiv_comp_eq [Normal K⟮t⟯ M] (ψ ψ' : F →ₐ[K] M) (hψ : ψ x = t)
    (hψ' : ψ' x = t) : ∃ τ : M ≃ₐ[K⟮t⟯] M, ∀ f, τ (ψ f) = ψ' f

theorem

restrictAlong_comp

L484 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.restrictAlong_comp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)
attribute [local instance] placeAction

Lean source · statement

theorem restrictAlong_comp (ψ : F →ₐ[K] M) (τ : M ≃ₐ[K⟮t⟯] M)
    (h₁ : (((τ : M →ₐ[K⟮t⟯] M).restrictScalars K).comp ψ).toRingHom.IsIntegral)
    (h₂ : ψ.toRingHom.IsIntegral) (W : Place K M) :
    W.restrictAlong (((τ : M →ₐ[K⟮t⟯] M).restrictScalars K).comp ψ) h₁ =
      (τ⁻¹ • W).restrictAlong ψ h₂

theorem

finiteAlong_norm

L495 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.finiteAlong_norm

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)
attribute [local instance] placeAction

Lean source · statement

theorem finiteAlong_norm [FiniteDimensional K⟮t⟯ M] (ψ : F →ₐ[K] M) (hψ : ψ x = t) :
    FiniteAlong K ψ

theorem

separableAlong_norm

L500 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.separableAlong_norm

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)
attribute [local instance] placeAction

Lean source · statement

theorem separableAlong_norm [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M] (ψ : F →ₐ[K] M)
    (hψ : ψ x = t) : SeparableAlong K ψ

theorem

isGalois_along

L505 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.isGalois_along

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section AlongPsi
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  (x : F) (t : M)
attribute [local instance] placeAction

Lean source · statement

theorem isGalois_along [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M] (ψ : F →ₐ[K] M)
    (hψ : ψ x = t) : @IsGalois F _ M _ (algebraAlong ψ)

theorem

algebraMap_gen_sub

L526 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.algebraMap_gen_sub

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
omit [IsAlgClosed K] [FiniteDimensional (↥K⟮t⟯) M] [IsGalois (↥K⟮t⟯) M] in

Lean source · statement

theorem algebraMap_gen_sub :
    algebraMap K⟮t⟯ M (IntermediateField.AdjoinSimple.gen K t - algebraMap K K⟮t⟯ j₀) =
      t - algebraMap K M j₀

theorem

transcendental_t

L532 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.transcendental_t

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
include hW₀ in
omit [FiniteDimensional (↥K⟮t⟯) M] [IsGalois (↥K⟮t⟯) M] in

Lean source · statement

theorem transcendental_t : Transcendental K t

theorem

psi_sub

L540 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.psi_sub

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
omit [IsAlgClosed K] [FiniteDimensional (↥K⟮t⟯) M] [IsGalois (↥K⟮t⟯) M] in

Lean source · statement

theorem psi_sub (ψ : F →ₐ[K] M) (hψ : ψ x = t) : ψ (x - algebraMap K F j₀) = t - algebraMap K M j₀

theorem

ord_eq_card_stabilizer

L544 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.ord_eq_card_stabilizer

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
include hW₀ in

Lean source · statement

theorem ord_eq_card_stabilizer :
    W₀.ord (t - algebraMap K M j₀) = Nat.card (MulAction.stabilizer (M ≃ₐ[K⟮t⟯] M) W₀)

theorem

ord_restrictAlong_pos

L558 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.ord_restrictAlong_pos

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
include hW₀ in
omit [IsAlgClosed K] [FiniteDimensional (↥K⟮t⟯) M] [IsGalois (↥K⟮t⟯) M] in

Lean source · statement

theorem ord_restrictAlong_pos (ψ : F →ₐ[K] M) (hψ : ψ x = t) (h : ψ.toRingHom.IsIntegral) :
    0 < (W₀.restrictAlong ψ h).ord (x - algebraMap K F j₀)

theorem

exists_smul_eq_of_ord_pos

L565 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.exists_smul_eq_of_ord_pos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
include hW₀ in

Lean source · statement

theorem exists_smul_eq_of_ord_pos (W : Place K M) (hW : 0 < W.ord (t - algebraMap K M j₀)) :
    ∃ σ : M ≃ₐ[K⟮t⟯] M, σ • W₀ = W

theorem

inv_comp_apply

L572 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.inv_comp_apply

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
omit [IsAlgClosed K] [FiniteDimensional (↥K⟮t⟯) M] [IsGalois (↥K⟮t⟯) M] in

Lean source · statement

theorem inv_comp_apply (σ : M ≃ₐ[K⟮t⟯] M) (hι : ι x = t) :
    (((σ⁻¹ : M ≃ₐ[K⟮t⟯] M) : M →ₐ[K⟮t⟯] M).restrictScalars K).comp ι x = t

theorem

exists_restrictAlong_eq

L578 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.exists_restrictAlong_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
include hι hW₀ in

Lean source · statement

theorem exists_restrictAlong_eq (w : Place K F) (hw : 0 < w.ord (x - algebraMap K F j₀)) :
    ∃ (ψ : F →ₐ[K] M) (hψ : ψ x = t), W₀.restrictAlong ψ (hint ψ hψ) = w

def

toGal

L599 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.toGal

Documentation

A ring automorphism fixing the embedded field, regarded as an automorphism over the simple subfield.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction

Lean source · statement

def toGal (ψ : F →ₐ[K] M) (hψ : ψ x = t) (u : M ≃+* M) (hu : ∀ f, u (ψ f) = ψ f) :
    M ≃ₐ[K⟮t⟯] M

theorem

toGal_apply

L606 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.toGal_apply

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
omit [IsAlgClosed K] [FiniteDimensional (↥K⟮t⟯) M] [IsGalois (↥K⟮t⟯) M] in

Lean source · statement

theorem toGal_apply (ψ : F →ₐ[K] M) (hψ : ψ x = t) (u : M ≃+* M)
    (hu : ∀ f, u (ψ f) = ψ f) (y : M) : toGal x t ψ hψ u hu y = u y

theorem

restrictAlong_eq_iff

L609 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.restrictAlong_eq_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
omit [IsAlgClosed K] in

Lean source · statement

theorem restrictAlong_eq_iff (ψ ψ' : F →ₐ[K] M) (hψ : ψ x = t) (hψ' : ψ' x = t) :
    W₀.restrictAlong ψ (hint ψ hψ) = W₀.restrictAlong ψ' (hint ψ' hψ') ↔
      ∃ σ : M ≃ₐ[K⟮t⟯] M, SemilinearAut.ofAlgAut (σ.restrictScalars K) • W₀ = W₀ ∧
        ψ' = ((σ : M →ₐ[K⟮t⟯] M).restrictScalars K).comp ψ

abbrev

Emb

L647 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.Emb

Documentation

The embeddings that send the selected generator to the prescribed target element.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction

Lean source · statement

abbrev Emb : Type _

def

embAction

L650 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.embAction

Documentation

The action by postcomposition of simple-subfield automorphisms on the selected embeddings.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction

Lean source · full declaration

def embAction : MulAction (M ≃ₐ[K⟮t⟯] M) (Emb x t (K := K)) where
  smul σ ψ := ⟨((σ : M →ₐ[K⟮t⟯] M).restrictScalars K).comp ψ.1, by
    change σ (ψ.1 x) = t
    rw [ψ.2]
    exact σ.commutes (⟨t, IntermediateField.mem_adjoin_simple_self K t⟩ : K⟮t⟯)⟩
  one_smul ψ := Subtype.ext (AlgHom.ext fun _ => rfl)
  mul_smul σ τ ψ := Subtype.ext (AlgHom.ext fun _ => rfl)

theorem

smul_emb_val

L661 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.smul_emb_val

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
attribute [local instance] embAction
omit [IsAlgClosed K] [FiniteDimensional (↥K⟮t⟯) M] [IsGalois (↥K⟮t⟯) M] in

Lean source · statement

theorem smul_emb_val (σ : M ≃ₐ[K⟮t⟯] M) (ψ : Emb x t (K := K)) :
    (σ • ψ).1 = ((σ : M →ₐ[K⟮t⟯] M).restrictScalars K).comp ψ.1

theorem

setOf_sameClass_eq_orbit

L664 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.setOf_sameClass_eq_orbit

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
attribute [local instance] embAction
omit [IsAlgClosed K] in

Lean source · statement

theorem setOf_sameClass_eq_orbit (ψ : Emb x t (K := K)) :
    {ψ' : Emb x t (K := K) | W₀.restrictAlong ψ'.1 (hint ψ'.1 ψ'.2) = W₀.restrictAlong ψ.1 (hint
      ψ.1 ψ.2)} =
      MulAction.orbit (MulAction.stabilizer (M ≃ₐ[K⟮t⟯] M) W₀) ψ

theorem

card_stabilizer_emb

L677 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.card_stabilizer_emb

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
attribute [local instance] embAction
include hW₀ in

Lean source · statement

theorem card_stabilizer_emb (ψ : Emb x t (K := K)) :
    Nat.card (MulAction.stabilizer (MulAction.stabilizer (M ≃ₐ[K⟮t⟯] M) W₀) ψ) =
      Place.ramificationIndexAlong ψ.1 W₀

theorem

ord_restrictAlong_eq_card

L715 ↗

AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois.ProofAuxKcA.HilbertB.ord_restrictAlong_eq_card

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
noncomputable section
namespace ProofAuxKcA
namespace HilbertB
section Main
variable {K : Type*} [Field K] [IsAlgClosed K] {F M : Type*} [Field F] [Field M] [Algebra K F]
  [Algebra K M] (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
  [FiniteDimensional K⟮t⟯ M] [IsGalois K⟮t⟯ M]
  (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
  (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀))
attribute [local instance] placeAction
attribute [local instance] embAction
include hW₀ in

Lean source · statement

theorem ord_restrictAlong_eq_card (ψ : F →ₐ[K] M) (hψ : ψ x = t) :
    (W₀.restrictAlong ψ (hint ψ hψ)).ord (x - algebraMap K F j₀) =
      Nat.card {ψ' : Emb x t (K := K) //
        W₀.restrictAlong ψ'.1 (hint ψ'.1 ψ'.2) = W₀.restrictAlong ψ (hint ψ hψ)}

theorem

ord_restrictAlong_eq_natCard_algHom_of_isGalois

L754 ↗

AlgebraicCurve.Place.ord_restrictAlong_eq_natCard_algHom_of_isGalois

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_restrictAlong_eq_natCard_algHom_of_isGalois
open AlgebraicCurve IsDedekindDomain WithZero
open scoped IntermediateField
universe u v in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_restrictAlong_eq_natCard_algHom_of_isGalois
    (K : Type u) [Field K] [IsAlgClosed K]
    {F M : Type v} [Field F] [Field M] [Algebra K F] [Algebra K M]
    (x : F) (t : M) (j₀ : K) (ι : F →ₐ[K] M) (hι : ι x = t)
    (hfin : FiniteDimensional K⟮t⟯ M) (hgal : IsGalois K⟮t⟯ M)
    (hint : ∀ ψ : F →ₐ[K] M, ψ x = t → ψ.toRingHom.IsIntegral)
    (W₀ : Place K M) (hW₀ : 0 < W₀.ord (t - algebraMap K M j₀)) :
    (W₀.ord (t - algebraMap K M j₀) =
        Nat.card {σ : M ≃ₐ[K⟮t⟯] M // SemilinearAut.ofAlgAut (σ.restrictScalars K) • W₀ = W₀}) ∧
    (∀ (ψ : F →ₐ[K] M) (hψ : ψ x = t),
        0 < (W₀.restrictAlong ψ (hint ψ hψ)).ord (x - algebraMap K F j₀)) ∧
    (∀ w : Place K F, 0 < w.ord (x - algebraMap K F j₀) →
        ∃ (ψ : F →ₐ[K] M) (hψ : ψ x = t), W₀.restrictAlong ψ (hint ψ hψ) = w) ∧
    (∀ (ψ ψ' : F →ₐ[K] M) (hψ : ψ x = t) (hψ' : ψ' x = t),
        W₀.restrictAlong ψ (hint ψ hψ) = W₀.restrictAlong ψ' (hint ψ' hψ') ↔
          ∃ σ : M ≃ₐ[K⟮t⟯] M, SemilinearAut.ofAlgAut (σ.restrictScalars K) • W₀ = W₀ ∧
            ψ' = ((σ : M →ₐ[K⟮t⟯] M).restrictScalars K).comp ψ) ∧
    (∀ (ψ : F →ₐ[K] M) (hψ : ψ x = t),
        (W₀.restrictAlong ψ (hint ψ hψ)).ord (x - algebraMap K F j₀) =
          Nat.card {ψ' : {ψ' : F →ₐ[K] M // ψ' x = t} //
            W₀.restrictAlong ψ'.1 (hint ψ'.1 ψ'.2) = W₀.restrictAlong ψ (hint ψ hψ)})

Module documentation

Place ord restrict Along eq nat Card alg Hom of is Galois

Declarations