Module

CommAlgIdealWildSubgroup.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgIdealWildSubgroup

4 declarations indexed from sourceView source ↗

Module documentation

Native coefficient-algebra owner of the intrinsic wild subgroup

This is the same existing principal-unit subgroup. Its raw automorphism Group and action are retained inside the native owner, so original field consumers do not reopen them beside their scalar towers.

Imports5

Imported by3

theorem

commAlgIdealInertiaGroup_finite

EtaleFundamentalGroups.Inertia.commAlgIdealInertiaGroup_finite

Documentation

Finite coefficient automorphisms give finite intrinsic ideal inertia.

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 commAlgIdealInertiaGroup_finite
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [Finite (B.carrier ≃ₐ[A] B.carrier)] (Q : Ideal B.carrier) :
    Finite (commAlgIdealInertiaGroup A B Q).carrier

def

commAlgIdealWildSubgroup

EtaleFundamentalGroups.Inertia.commAlgIdealWildSubgroup

Documentation

The intrinsic principal-unit wild subgroup on the native inertia carrier.

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

def commAlgIdealWildSubgroup
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B.carrier]
    (Q : Ideal B.carrier) [Q.IsPrime] (hQ : Q ≠ ⊥) :
    Subgroup (commAlgIdealInertiaGroup A B Q).carrier

theorem

commAlgIdealWildSubgroup_card

EtaleFundamentalGroups.Inertia.commAlgIdealWildSubgroup_card

Documentation

Its literal cardinality is the independently computed wild order.

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_card
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B.carrier]
    (Q : Ideal B.carrier) [Q.IsPrime] (hQ : Q ≠ ⊥) :
    Nat.card (commAlgIdealWildSubgroup A B Q hQ) = commAlgIdealWildOrder A B Q hQ

theorem

commAlgIdealWildSubgroup_index

EtaleFundamentalGroups.Inertia.commAlgIdealWildSubgroup_index

Documentation

Its index is the same independently computed tame degree.

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
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B.carrier]
    (Q : Ideal B.carrier) [Q.IsPrime] (hQ : Q ≠ ⊥) :
    (commAlgIdealWildSubgroup A B Q hQ).index = commAlgIdealTameOrder A B Q hQ