Module

FiniteOriginalCanonicalTameExactness.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteOriginalCanonicalTameExactness

2 declarations indexed from sourceView source ↗

Module documentation

Exactness of original finite canonical characters

Identifies the kernel of the canonical finite normalization character with original wild inertia and proves surjectivity onto the full roots group.

Imports2

Imported by2

theorem

finiteOriginalCanonicalTameCharacter_ker

L30 ↗

EtaleFundamentalGroups.Inertia.finiteOriginalCanonicalTameCharacter_ker

Documentation

The constructed canonical finite character has exactly the actual original wild inertia kernel, with all normalization arithmetic proved.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
variable (A : Type u) (B : Type v)
  [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
  [CommRing B] [IsDedekindDomain B] [Algebra A B]
  [Module.Finite A B] [Module.IsTorsionFree A B]
  [IsGaloisGroup (B ≃ₐ[A] B) A B]
  (Q : Ideal B) [Q.IsMaximal] [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥)

Lean source · statement

theorem finiteOriginalCanonicalTameCharacter_ker :
    (finiteIdealCanonicalTameCharacterGroupMap A B (B ≃ₐ[A] B) Q hQ).ker =
      finiteIdealWildSubgroup B (B ≃ₐ[A] B) Q hQ

theorem

finiteOriginalCanonicalTameCharacter_surjective

L39 ↗

EtaleFundamentalGroups.Inertia.finiteOriginalCanonicalTameCharacter_surjective