NYLL
Module

ActualFiniteWildProperties.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteWildProperties
5 declarations indexed from sourceView source ↗

Module documentation

Primary, characteristic-zero and index laws for actual finite wild inertia

The normalization group and field constructors are already closed. These proofs use only the actual subgroup's cardinality, actual tame/wild orders, and the original residue field.

Imports11
Imported by4

Declarations

theorem

actualFiniteWildSubgroup_card_exists_pow_of_baseResidue_charP

L42 ↗
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_card_exists_pow_of_baseResidue_charP
Documentation

The SAME actual finite wild subgroup has power-of-p cardinality.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
  [fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
  [aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
Lean source · statement
theorem actualFiniteWildSubgroup_card_exists_pow_of_baseResidue_charP
    (E : FiniteGaloisIntermediateField K L)
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p] :
    ∃ n : ℕ, Nat.card (actualFiniteWildSubgroup A K L Q E) = p ^ n
theorem

actualFiniteWildSubgroup_isPGroup_of_baseResidue_charP

L51 ↗
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_isPGroup_of_baseResidue_charP
Documentation

Its cardinality supplies the p-group property.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
  [fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
  [aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
Lean source · statement
theorem actualFiniteWildSubgroup_isPGroup_of_baseResidue_charP
    (E : FiniteGaloisIntermediateField K L)
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p] :
    IsPGroup p (actualFiniteWildSubgroup A K L Q E)
theorem

actualFiniteWildSubgroup_eq_bot_of_baseResidue_charZero

L60 ↗
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_eq_bot_of_baseResidue_charZero
Documentation

In characteristic zero of the original base residue field, the same actual intrinsic finite wild subgroup is trivial.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
  [fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
  [aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
Lean source · statement
theorem actualFiniteWildSubgroup_eq_bot_of_baseResidue_charZero
    (E : FiniteGaloisIntermediateField K L) [CharZero (IsLocalRing.ResidueField A)] :
    actualFiniteWildSubgroup A K L Q E = ⊥
theorem

actualFiniteWildSubgroup_index_isUnit

L69 ↗
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_index_isUnit
Documentation

The actual intrinsic wild index is invertible in the original DVR.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
  [fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
  [aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
Lean source · statement
theorem actualFiniteWildSubgroup_index_isUnit (E : FiniteGaloisIntermediateField K L) :
    IsUnit ((actualFiniteWildSubgroup A K L Q E).index : A)
theorem

actualFiniteWildSubgroup_index_not_dvd_of_baseResidue_charP

L75 ↗
EtaleFundamentalGroups.Inertia.actualFiniteWildSubgroup_index_not_dvd_of_baseResidue_charP
Documentation

The same subgroup has index prime to the original residue characteristic.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
  [fK : Field K] [fL : Field L] [aAK : Algebra A K] [frAK : IsFractionRing A K]
  [aKL : Algebra K L] [aAL : Algebra A L] [tAKL : IsScalarTower A K L] [gKL : IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [qMax : Q.IsMaximal]
Lean source · statement
theorem actualFiniteWildSubgroup_index_not_dvd_of_baseResidue_charP
    (E : FiniteGaloisIntermediateField K L) :
    ∀ (p : ℕ) [CharP (IsLocalRing.ResidueField A) p],
      ¬ p ∣ (actualFiniteWildSubgroup A K L Q E).index

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