Module

ActualFiniteCanonicalTameKernel.lean

Nyll.EtaleFundamentalGroups.Inertia.ActualFiniteCanonicalTameKernel

1 declaration indexed from sourceView source ↗

Module documentation

The actual normalized finite character has the actual wild kernel

The already proved actual finite arithmetic supplies coprimality of n and e/n. The native coefficient theorem proves that this actual normalization preserves the independent principal-unit kernel.

Imports10

Imported by2

theorem

actualFiniteCanonicalTameMorphism_ker

L40 ↗

EtaleFundamentalGroups.Inertia.actualFiniteCanonicalTameMorphism_ker

Documentation

The SAME e/n-normalized canonical character has the independently constructed principal-unit subgroup as kernel.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
  (Q : Ideal (normalizationCommAlgCat A L).carrier) [Q.IsMaximal]

Lean source · statement

theorem actualFiniteCanonicalTameMorphism_ker (E : FiniteGaloisIntermediateField K L) :
    (actualFiniteCanonicalTameMorphism A K L Q E).hom'.ker =
      actualFiniteWildSubgroup A K L Q E

Module documentation

The actual normalized finite character has the actual wild kernel

Declarations

actualFiniteCanonicalTameMorphism_ker