NYLL
Module

OriginalFiniteFieldWildResiduePrimary.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalFiniteFieldWildResiduePrimary
4 declarations indexed from sourceView source ↗

Module documentation

Original finite wild inertia over the base residue characteristic

The independent original-field wild subgroup has prime-power cardinality for the characteristic of the base DVR residue field. The same subgroup is a p-group in positive residue characteristic and is trivial when that base residue field has characteristic zero.

Imports6
Imported by1

Declarations

theorem

originalFiniteFieldWildSubgroup_card_exists_baseResidue_expChar_pow

L33 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup_card_exists_baseResidue_expChar_pow
Documentation

The original finite-field wild subgroup has power cardinality for the exponential characteristic of the original base 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_baseResidue_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 (IsLocalRing.ResidueField A)) ^ r
theorem

originalFiniteFieldWildSubgroup_card_exists_pow_of_baseResidue_charP

L48 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup_card_exists_pow_of_baseResidue_charP
Documentation

For the positive prime characteristic of the base residue field, the SAME original finite-field wild subgroup has a power-of-p cardinality.

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_pow_of_baseResidue_charP
    (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]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p] :
    ∃ r : ℕ, Nat.card (originalFiniteFieldWildSubgroup A K F Q) = p ^ r
theorem

originalFiniteFieldWildSubgroup_isPGroup_of_baseResidue_charP

L62 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup_isPGroup_of_baseResidue_charP
Documentation

The independent original-field wild group is a p-group for the prime characteristic of the original base 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_isPGroup_of_baseResidue_charP
    (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]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p] :
    IsPGroup p (originalFiniteFieldWildSubgroup A K F Q)
theorem

originalFiniteFieldWildSubgroup_eq_bot_of_baseResidue_charZero

L77 ↗
EtaleFundamentalGroups.Inertia.originalFiniteFieldWildSubgroup_eq_bot_of_baseResidue_charZero
Documentation

In characteristic zero of the base residue field, the SAME original finite-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_baseResidue_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 (IsLocalRing.ResidueField A)] :
    originalFiniteFieldWildSubgroup A K F Q = ⊥

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