NYLL
Module

CommAlgCanonicalTameCoprimeExactness.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgCanonicalTameCoprimeExactness
1 declaration indexed from sourceView source ↗

Module documentation

Exactness of the SAME canonical character from normalization coprimality

The existing primitive root determines the full root-group cardinality. Mathlib's coprime-power bijection then proves that the actual e/n power normalization preserves surjectivity and the independently defined wild kernel.

Imports10
Imported by3

Declarations

theorem

commAlgCanonicalTameMorphism_exact_of_coprime

L34 ↗
EtaleFundamentalGroups.Inertia.commAlgCanonicalTameMorphism_exact_of_coprime
Documentation

Coprimality of the actual tame order and actual e/n normalization exponent makes the SAME normalized character onto with its SAME principal-unit kernel.

Source context 3 commands

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

open scoped Pointwise
namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgCanonicalTameMorphism_exact_of_coprime
    (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 ≠ ⊥)
    (hcop : Nat.Coprime (commAlgIdealTameOrder A B q hq)
      (q.ramificationIdx A / commAlgIdealTameOrder A B q hq)) :
    Function.Surjective (commAlgCanonicalTameMorphism A B q hq).hom'.toFun ∧
      (commAlgCanonicalTameMorphism A B q hq).hom'.ker =
        commAlgIdealWildSubgroup A B q hq

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