NYLL
Module

NatCard_place_ord_sub_pos_le_natCard_doubleCoset.lean

Nyll.AlgebraicCurves.Places.NatCard_place_ord_sub_pos_le_natCard_doubleCoset
5 declarations indexed from sourceView source ↗

Module documentation

Nat Card place ord sub pos le nat Card double Coset

Imports5
Imported by1

Declarations

theorem

apply_eq_self_of_mem_adjoin

L55 ↗
AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset.AlgebraicCurve.PlacesLeDoubleCoset.apply_eq_self_of_mem_adjoin
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
open _root_.AlgebraicCurve
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlacesLeDoubleCoset
open _root_.AlgebraicCurve
variable {K : Type*} [Field K] {L : Type*} [Field L] [Algebra K L]
Lean source · statement
theorem apply_eq_self_of_mem_adjoin (ψ : L →ₐ[K] L) (t : L) (hψ : ψ t = t) {x : L}
    (hx : x ∈ K⟮t⟯) : ψ x = x
theorem

algHom_apply_algebraMap

L72 ↗
AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset.AlgebraicCurve.PlacesLeDoubleCoset.algHom_apply_algebraMap
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
open _root_.AlgebraicCurve
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlacesLeDoubleCoset
open _root_.AlgebraicCurve
variable {K : Type*} [Field K] {L : Type*} [Field L] [Algebra K L]
Lean source · statement
theorem algHom_apply_algebraMap (t : L) (E : IntermediateField K⟮t⟯ L) (x : E) (hx : (x : L) = t)
    (ψ : E →ₐ[K] L) (hψ : ψ x = t) (l : K⟮t⟯) : ψ (algebraMap K⟮t⟯ E l) = l
theorem

isIntegral_of_apply_eq_sub

L92 ↗
AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset.AlgebraicCurve.PlacesLeDoubleCoset.isIntegral_of_apply_eq_sub
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
open _root_.AlgebraicCurve
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlacesLeDoubleCoset
open _root_.AlgebraicCurve
variable {K : Type*} [Field K] {L : Type*} [Field L] [Algebra K L]
Lean source · statement
theorem isIntegral_of_apply_eq_sub (t : L) [FiniteDimensional K⟮t⟯ L]
    (E : IntermediateField K⟮t⟯ L) (x : E) (hx : (x : L) = t)
    (ψ : E →ₐ[K] L) (hψ : ψ x = t) : ψ.toRingHom.IsIntegral
theorem

finite_doubleCosetQuotient

L105 ↗
AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset.AlgebraicCurve.PlacesLeDoubleCoset.finite_doubleCosetQuotient
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
open _root_.AlgebraicCurve
open scoped IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlacesLeDoubleCoset
open _root_.AlgebraicCurve
variable {K : Type*} [Field K] {L : Type*} [Field L] [Algebra K L]
Lean source · statement
theorem finite_doubleCosetQuotient {Γ₀ : Type*} [Group Γ₀] (Γ Kst : Subgroup Γ₀) [Γ.FiniteIndex] :
    Finite (DoubleCoset.Quotient (Γ : Set Γ₀) (Kst : Set Γ₀))
theorem

natCard_place_ord_sub_pos_le_natCard_doubleCoset

L129 ↗
AlgebraicCurve.natCard_place_ord_sub_pos_le_natCard_doubleCoset
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.NatCard_place_ord_sub_pos_le_natCard_doubleCoset
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
  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
open _root_.AlgebraicCurve
open scoped IntermediateField
open _root_.AlgebraicCurve
open scoped IntermediateField
open NatCard_place_ord_sub_pos_le_natCard_doubleCoset.AlgebraicCurve.PlacesLeDoubleCoset in
Lean source · statement
theorem _root_.AlgebraicCurve.natCard_place_ord_sub_pos_le_natCard_doubleCoset
    (K : Type*) [Field K] [IsAlgClosed K] {L : Type*} [Field L] [Algebra K L]
    (t : L) (hfin : FiniteDimensional K⟮t⟯ L) (hgal : IsGalois K⟮t⟯ L)
    {Γ₀ : Type*} [Group Γ₀] (σ : Γ₀ →* (L ≃ₐ[K⟮t⟯] L)) (hσ : Function.Surjective σ)
    (Γ Kst : Subgroup Γ₀) [Γ.FiniteIndex]
    (E : IntermediateField K⟮t⟯ L) (hE : ∀ γ ∈ Γ, ∀ e : E, σ γ (e : L) = e)
    (c : K) (W : AlgebraicCurve.Place K L) (hW : 0 < W.ord (t - algebraMap K L c))
    (hD : ∀ k ∈ Kst, AlgebraicCurve.SemilinearAut.ofAlgAut ((σ k).restrictScalars K) • W = W)
    (x : E) (hx : (x : L) = t) :
    Nat.card {P : AlgebraicCurve.Place K E // 0 < P.ord (x - algebraMap K E c)} ≤
      Nat.card (DoubleCoset.Quotient (Γ : Set Γ₀) (Kst : Set Γ₀))

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