NYLL
Module

OriginalFiniteFieldWildCardinality.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteFieldWildCardinality
6 declarations indexed from sourceView source ↗

Module documentation

Cardinality of the original finite-field wild subgroup

The genuine normalization restriction equivalence preserves the cardinality of the already-defined wild comap and its inertia quotient. This yields the literal original-field wild-order and tame-order statements.

Imports11
Imported by2

Declarations

theorem

card_comap_mulEquiv

L35 ↗
EtaleFundamentalGroups.Inertia.card_comap_mulEquiv
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem card_comap_mulEquiv
    {G : Type u} {H : Type v} [Group G] [Group H]
    (e : G ≃* H) (P : Subgroup H) :
    Nat.card (P.comap e.toMonoidHom) = Nat.card P
theorem

card_quotient_comap_mulEquiv

L42 ↗
EtaleFundamentalGroups.Inertia.card_quotient_comap_mulEquiv
Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem card_quotient_comap_mulEquiv
    {G : Type u} {H : Type v} [Group G] [Group H]
    (e : G ≃* H) (P : Subgroup H) :
    Nat.card (G ⧸ P.comap e.toMonoidHom) = Nat.card (H ⧸ P)
theorem

originalFiniteFieldWildSubgroup_card

L51 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup_card
Documentation

Cardinality transports through the actual normalization restriction equivalence to the SAME original-field wild subgroup, which was defined independently as a comap.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem originalFiniteFieldWildSubgroup_card
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field F] [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal] :
    Nat.card (originalFiniteFieldWildSubgroup A K F Q) =
      Nat.card (originalFiniteNormalizationWildSubgroup A K F Q)
theorem

originalFiniteFieldWildSubgroup_card_exists_expChar_pow

L65 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup_card_exists_expChar_pow
Documentation

The literal original finite-field wild subgroup has order a power of the exponential characteristic of its actual normalization residue field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem originalFiniteFieldWildSubgroup_card_exists_expChar_pow
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field F] [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal] :
    ∃ r : ℕ, Nat.card (originalFiniteFieldWildSubgroup A K F Q) =
      (ringExpChar Q.ResidueField) ^ r
theorem

originalFiniteFieldWildSubgroup_eq_bot_of_charZero

L79 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup_eq_bot_of_charZero
Documentation

In residue characteristic zero, the SAME independently defined original-field wild subgroup is trivial.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem originalFiniteFieldWildSubgroup_eq_bot_of_charZero
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field F] [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal]
    [CharZero Q.ResidueField] :
    originalFiniteFieldWildSubgroup A K F Q = ⊥
theorem

originalFiniteFieldTameOrder_eq_card_quotient_wild

L95 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldTameOrder_eq_card_quotient_wild
Documentation

The same actual tame degree used by the original finite canonical character is exactly the cardinality of original inertia modulo its SAME independently defined wild subgroup.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · full declaration
theorem originalFiniteFieldTameOrder_eq_card_quotient_wild
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field F] [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [FiniteDimensional K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F)) [Q.IsMaximal] :
    let : IsDedekindDomain (normalizationCommAlgCat A F) :=
      integralClosure.isDedekindDomain A K F
    commAlgIdealTameOrder A (normalizationCommAlgCat A F) Q
        (originalFiniteNormalizationPrime_ne_bot A K F Q) =
      Nat.card (actualNormalizationInertiaGroup A K F Q ⧸
        originalFiniteFieldWildSubgroup A K F Q) := by
  have dB : IsDedekindDomain (normalizationCommAlgCat A F) :=
    integralClosure.isDedekindDomain A K F
  exact (originalFiniteNormalizationTameOrder_eq_card_quotient_wild A K F Q).trans
    (card_quotient_comap_mulEquiv (originalFiniteNormalizationInertiaEquiv A K F Q)
      (originalFiniteNormalizationWildSubgroup A K F Q)).symm

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