NYLL
Module

Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.lean

Nyll.AlgebraicCurves.Places.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
22 declarations indexed from sourceView source ↗

Module documentation

Place ncard alg Hom comp eq preimage eq ramification Index Along

Imports6
Imported by2

Declarations

theorem

ncard_preimage_eq_mul

L52 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.ncard_preimage_eq_mul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
Lean source · statement
theorem ncard_preimage_eq_mul {G T : Type*} [Finite G] (Θ : G → T) (p : Set T) (hp : p.Finite)
    (h : ℕ) (hfib : ∀ t ∈ p, Set.ncard {g | Θ g = t} = h) :
    Set.ncard {g | Θ g ∈ p} = h * p.ncard
def

toAutK

L79 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.toAutK
Documentation

The group homomorphism viewing automorphisms over the extension field as base-field automorphisms.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
Lean source · full declaration
def toAutK : (M ≃ₐ[F] M) →* (M ≃ₐ[K] M) where
  toFun g := g.restrictScalars K
  map_one' := AlgEquiv.ext fun _ => rfl
  map_mul' _ _ := AlgEquiv.ext fun _ => rfl
theorem

toAutK_apply

L84 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.toAutK_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem toAutK_apply (g : M ≃ₐ[F] M) (x : M) : toAutK (K := K) g x = g x
theorem

mem_smul_iff

L86 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.mem_smul_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem mem_smul_iff (g : M ≃ₐ[F] M) (W : Place K M) (x : M) :
    x ∈ (toAutK (K := K) g • W).toValuationSubring ↔ g⁻¹ x ∈ W.toValuationSubring
theorem

restrict_smul

L91 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.restrict_smul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem restrict_smul [Algebra.IsIntegral F M] (g : M ≃ₐ[F] M) (W : Place K M) :
    (toAutK (K := K) g • W).restrict F = W.restrict F
theorem

restrict_restrict

L96 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.restrict_restrict
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
Lean source · statement
theorem restrict_restrict {F' : Type*} [Field F'] [Algebra K F'] [Algebra F F'] [Algebra F' M]
    [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower F F' M]
    [Algebra.IsIntegral F F'] [Algebra.IsIntegral F' M] [Algebra.IsIntegral F M] (W : Place K M) :
    (W.restrict F').restrict F = W.restrict F
theorem

exists_smul_eq_of_restrict_eq

L106 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.exists_smul_eq_of_restrict_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem exists_smul_eq_of_restrict_eq (W W' : Place K M) (h : W'.restrict F = W.restrict F) :
    ∃ g : M ≃ₐ[F] M, toAutK (K := K) g • W = W'
theorem

ncard_setOf_smul_eq

L134 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.ncard_setOf_smul_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem ncard_setOf_smul_eq (W₁ W : Place K M) (h : W.restrict F = W₁.restrict F) :
    Set.ncard {g : M ≃ₐ[F] M | toAutK (K := K) g • W₁ = W} =
      Set.ncard {g : M ≃ₐ[F] M | toAutK (K := K) g • W₁ = W₁}
theorem

ncard_stabilizer

L150 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.ncard_stabilizer
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Galois
variable {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
  [Algebra F M] [IsScalarTower K F M]
variable [FiniteDimensional F M] [IsGalois F M]
Lean source · statement
theorem ncard_stabilizer [IsAlgClosed K] (W₁ : Place K M) :
    Set.ncard {g : M ≃ₐ[F] M | toAutK (K := K) g • W₁ = W₁} =
      W₁.ramificationIndex F * W₁.inertiaDeg F
theorem

inertiaDeg_eq_one

L180 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.inertiaDeg_eq_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Tower
variable {K F F' M : Type*} [Field K] [Field F] [Field F'] [Field M] [Algebra K F] [Algebra K F']
  [Algebra K M] [Algebra F F'] [Algebra F' M] [Algebra F M] [IsScalarTower K F F']
  [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
  [Algebra.IsIntegral F F'] [Algebra.IsIntegral F' M] [Algebra.IsIntegral F M]
Lean source · statement
theorem inertiaDeg_eq_one [IsAlgClosed K] [IsCurveOver K F] [IsCurveOver K M]
    (W : Place K M) : W.inertiaDeg F = 1
theorem

ramificationIndex_tower

L186 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.ramificationIndex_tower
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Tower
variable {K F F' M : Type*} [Field K] [Field F] [Field F'] [Field M] [Algebra K F] [Algebra K F']
  [Algebra K M] [Algebra F F'] [Algebra F' M] [Algebra F M] [IsScalarTower K F F']
  [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
  [Algebra.IsIntegral F F'] [Algebra.IsIntegral F' M] [Algebra.IsIntegral F M]
Lean source · statement
theorem ramificationIndex_tower (W : Place K M) :
    W.ramificationIndex F = W.ramificationIndex F' * (W.restrict F').ramificationIndex F
theorem

exists_restrict_eq

L204 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.exists_restrict_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Existence
variable {K F' M : Type*} [Field K] [Field F'] [Field M] [Algebra K F'] [Algebra K M]
  [Algebra F' M] [IsScalarTower K F' M] [FiniteDimensional F' M] [Algebra.IsSeparable F' M]
Lean source · statement
theorem exists_restrict_eq (q : Place K F') : ∃ W : Place K M, W.restrict F' = q
def

theta

L231 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.theta
Documentation

The embedding obtained by composing subfield inclusion, an automorphism, and the target embedding.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
Lean source · statement
def theta (ι : M →ₐ[F] E) (g : M ≃ₐ[F] M) : F' →ₐ[F] E
theorem

theta_apply

L234 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.theta_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
Lean source · statement
theorem theta_apply (ι : M →ₐ[F] E) (g : M ≃ₐ[F] M) (y : F') :
    theta ι g y = ι (g (algebraMap F' M y))
theorem

theta_mul_restrictScalars

L237 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.theta_mul_restrictScalars
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
Lean source · statement
theorem theta_mul_restrictScalars (ι : M →ₐ[F] E) (g : M ≃ₐ[F] M) (h : M ≃ₐ[F'] M) :
    theta ι (g * h.restrictScalars F) = theta (F' := F') ι g
theorem

setOf_theta_eq

L242 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.setOf_theta_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
Lean source · full declaration
theorem setOf_theta_eq (ι : M →ₐ[F] E) (g₀ : M ≃ₐ[F] M) :
    {g : M ≃ₐ[F] M | theta (F' := F') ι g = theta ι g₀} =
      (fun h : M ≃ₐ[F'] M => g₀ * h.restrictScalars F) '' Set.univ := by
  ext g
  simp only [Set.mem_ofPred_eq, Set.image_univ, Set.mem_range]
  constructor
  · intro hg
    have hfix : ∀ y : F', (g₀⁻¹ * g) (algebraMap F' M y) = algebraMap F' M y := by
      intro y
      have := congrArg (fun τ : F' →ₐ[F] E => τ y) hg
      simp only [theta_apply] at this
      rw [AlgEquiv.mul_apply, AlgEquiv.aut_inv, AlgEquiv.symm_apply_eq]
      exact ι.toRingHom.injective this
    refine ⟨{ (g₀⁻¹ * g).toRingEquiv with commutes' := hfix }, ?_⟩
    refine AlgEquiv.ext fun x => ?_
    change g₀ ((g₀⁻¹ * g) x) = g x
    rw [← AlgEquiv.mul_apply, mul_inv_cancel_left]
  · rintro ⟨h, rfl⟩
    exact theta_mul_restrictScalars ι g₀ h
theorem

theta_surjective

L264 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.theta_surjective
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
variable [FiniteDimensional F M] [IsGalois F M] [IsAlgClosed E]
Lean source · statement
theorem theta_surjective (ι : M →ₐ[F] E) : Function.Surjective (theta (F' := F') ι)
theorem

ncard_setOf_theta_eq

L287 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.ncard_setOf_theta_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
variable [FiniteDimensional F M] [IsGalois F M] [IsAlgClosed E]
Lean source · statement
theorem ncard_setOf_theta_eq (ι : M →ₐ[F] E) (τ : F' →ₐ[F] E) :
    Set.ncard {g : M ≃ₐ[F] M | theta ι g = τ} = Nat.card (M ≃ₐ[F'] M)
theorem

restrict_smul_eq_iff

L294 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.restrict_smul_eq_iff
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
variable [FiniteDimensional F M] [IsGalois F M] [IsAlgClosed E]
omit [IsScalarTower K F F'] [FiniteDimensional F M] [IsGalois F M] [IsAlgClosed E] in
Lean source · statement
theorem restrict_smul_eq_iff (ι : M →ₐ[F] E) (A : ValuationSubring E) (W₁ : Place K M)
    (hW₁ : W₁.toValuationSubring = A.comap ι.toRingHom) [Algebra.IsIntegral F' M]
    (g : M ≃ₐ[F] M) (q : Place K F') :
    (toAutK (K := K) g⁻¹ • W₁).restrict F' = q ↔
      ∀ y : F', y ∈ q.toValuationSubring ↔ theta ι g y ∈ A
theorem

ncard_setOf_forall_mem_iff

L308 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.ncard_setOf_forall_mem_iff
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
section Core
variable {K F F' M E : Type*} [Field K] [Field F] [Field F'] [Field M] [Field E]
  [Algebra K F] [Algebra K F'] [Algebra K M]
  [Algebra F F'] [Algebra F' M] [Algebra F M] [Algebra F E]
  [IsScalarTower K F F'] [IsScalarTower K F' M] [IsScalarTower K F M] [IsScalarTower F F' M]
variable [FiniteDimensional F M] [IsGalois F M] [IsAlgClosed E]
Lean source · statement
theorem ncard_setOf_forall_mem_iff [IsAlgClosed K] [IsCurveOver K F] [IsCurveOver K F']
    [IsCurveOver K M] [FiniteDimensional F F']
    (ι : M →ₐ[F] E) (A : ValuationSubring E) (W₁ : Place K M)
    (hW₁ : W₁.toValuationSubring = A.comap ι.toRingHom) (q : Place K F')
    (hq : q.restrict F = W₁.restrict F) :
    Set.ncard {τ : F' →ₐ[F] E | ∀ y : F', y ∈ q.toValuationSubring ↔ τ y ∈ A} =
      q.ramificationIndex F
theorem

fg_of_finite

L374 ↗
AlgebraicCurves.Places.Proofs.Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong.AlgebraicCurve.SpecialisationCount.fg_of_finite
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace SpecialisationCount
Lean source · statement
theorem fg_of_finite {K F M : Type*} [Field K] [Field F] [Field M] [Algebra K F] [Algebra K M]
    [Algebra F M] [IsScalarTower K F M] [Module.Finite F M] {x : F} (hx : Transcendental K x)
    (hfinx : FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F) :
    Transcendental K (algebraMap F M x) ∧
      FiniteDimensional (IntermediateField.adjoin K ({algebraMap F M x} : Set M)) M
theorem

ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong

L403 ↗
AlgebraicCurve.Place.ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Place_ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
attribute [-instance]
  AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
  AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
  AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
  AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
  AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
  AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
  AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
  AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
open scoped Pointwise
open _root_.AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ncard_algHom_comp_eq_preimage_eq_ramificationIndexAlong
    (K F F' : Type*) [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
    [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [IsCurveOver K F']
    (hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ)
    (E : Type*) [Field E] [Algebra K E] [IsAlgClosed E]
    (A : ValuationSubring E) (e : F →ₐ[K] E) (v₀ : Place K F)
    (hev₀ : ∀ f : F, f ∈ v₀.toValuationSubring ↔ e f ∈ A)
    (q : Place K F') (hq : q.restrictAlong φ hφ = v₀) :
    Set.ncard {σ : F' →ₐ[K] E | σ.comp φ = e ∧
        ∀ g : F', g ∈ q.toValuationSubring ↔ σ g ∈ A} =
      q.ramificationIndexAlong φ

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