NYLL
Module

CommAlgIdealWildProperties.lean

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

Module documentation

Intrinsic wild subgroup laws on one coefficient algebra

The subgroup is literally the existing principal-unit subgroup in native coefficient-automorphism inertia. Its primary order, character kernel and tame quotient cardinality supply the three Sylow image inputs. No field presentation or comparison premise is introduced.

Imports14
Imported by2

Declarations

theorem

commAlgIdealWildSubgroup_isPGroup_of_baseResidue_charP

L39 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealWildSubgroup_isPGroup_of_baseResidue_charP
Documentation

The existing intrinsic principal-unit wild subgroup is a p-group for the characteristic of the original base residue field.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgIdealWildSubgroup_isPGroup_of_baseResidue_charP
    (A : Type u) [CommRing A] [IsDomain A] [IsLocalRing A]
    (B : CommAlgCat.{v} A) [IsDedekindDomain B.carrier]
    [Module.Finite A B.carrier] [Module.IsTorsionFree A B.carrier]
    (Q : Ideal B.carrier) [Q.IsPrime]
    [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥)
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField A) p] :
    IsPGroup p (finiteIdealWildSubgroup B.carrier
      (B.carrier ≃ₐ[A] B.carrier) Q hQ)
theorem

commAlgIdealWildSubgroup_normal

L60 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealWildSubgroup_normal
Documentation

The same intrinsic wild subgroup is normal because it is the proved kernel of the actual finite ideal tame character.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgIdealWildSubgroup_normal
    (A : Type u) [CommRing A]
    (B : CommAlgCat.{v} A) [IsDedekindDomain B.carrier]
    [Finite (B.carrier ≃ₐ[A] B.carrier)]
    (Q : Ideal B.carrier) [Q.IsPrime] (hQ : Q ≠ ⊥) :
    (finiteIdealWildSubgroup B.carrier
      (B.carrier ≃ₐ[A] B.carrier) Q hQ).Normal
theorem

commAlgIdealWildSubgroup_index_isUnit

L75 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealWildSubgroup_index_isUnit
Documentation

Its literal index is the existing tame quotient cardinality and is therefore invertible in the original local coefficient ring.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgIdealWildSubgroup_index_isUnit
    (A : Type u) [CommRing A] [IsLocalRing A]
    (B : CommAlgCat.{v} A) [IsDedekindDomain B.carrier]
    [Finite (B.carrier ≃ₐ[A] B.carrier)]
    (Q : Ideal B.carrier) [Q.IsPrime]
    [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥) :
    IsUnit ((finiteIdealWildSubgroup B.carrier
      (B.carrier ≃ₐ[A] B.carrier) Q hQ).index : A)
theorem

commAlgIdealWildSubgroup_index_not_dvd_of_baseResidue_charP

L93 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealWildSubgroup_index_not_dvd_of_baseResidue_charP
Documentation

The same intrinsic wild subgroup has prime-to-characteristic index. Only the already proved base-ring unit enters the residue calculation.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgIdealWildSubgroup_index_not_dvd_of_baseResidue_charP
    (A : Type u) [CommRing A] [IsLocalRing A]
    (B : CommAlgCat.{v} A) [IsDedekindDomain B.carrier]
    [Finite (B.carrier ≃ₐ[A] B.carrier)]
    (Q : Ideal B.carrier) [Q.IsPrime]
    [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥)
    (p : ℕ) [CharP (IsLocalRing.ResidueField A) p] :
    ¬ p ∣ (finiteIdealWildSubgroup B.carrier
      (B.carrier ≃ₐ[A] B.carrier) Q hQ).index

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