NYLL
Module

CommAlgIdealTameOrder.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgIdealTameOrder
2 declarations indexed from sourceView source ↗

Module documentation

Intrinsic tame and wild orders

Defines the tame order and principal-unit kernel order for the canonical coefficient- automorphism action on a native normalization algebra.

Imports3
Imported by15

Declarations

def

commAlgIdealTameOrder

L26 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealTameOrder
Documentation

The intrinsic actual tame order of a native normalization algebra, with its original coefficient automorphisms acting canonically.

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

commAlgIdealWildOrder

L31 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealWildOrder
Documentation

The intrinsic actual principal-unit kernel order for the same action.

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

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