Module

CommAlgCanonicalTameCompositeEvaluation.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgCanonicalTameCompositeEvaluation

5 declarations indexed from sourceView source ↗

Module documentation

Scalar evaluation of tame character composites

Evaluates a precomposed canonical tame character followed by a residue ring map. Supplies the corresponding local coefficient map and a uniformizer-ratio witness.

Imports3

Imported by2

def

commAlgCanonicalTameCompositeValue

L28 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameCompositeValue

Documentation

The scalar value of the SAME precomposition, canonical character, and literal residue RingHom. A pointwise source needs no group structure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification
universe u v w

Lean source · statement

def commAlgCanonicalTameCompositeValue
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
    {I : Type w} (r : I → commAlgIdealInertiaGroup A B Q)
    {k : Type v} [CommRing k] (i : Q.ResidueField →+* k) (σ : I) : k

theorem

commAlgCanonicalTameCompositeValue_eq_projection

L38 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameCompositeValue_eq_projection

Documentation

Explicit scalar projection of the existing rootsGroupMap composite. Neither the character nor the coefficient roots map is replaced.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification
universe u v w

Lean source · full declaration

theorem commAlgCanonicalTameCompositeValue_eq_projection
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
    {I : Type w} (r : I → commAlgIdealInertiaGroup A B Q)
    {k : Type v} [CommRing k] (i : Q.ResidueField →+* k) (σ : I) :
    commAlgCanonicalTameCompositeValue A B Q hQ r i σ =
      (show rootsOfUnity (commAlgIdealTameOrder A B Q hQ) k from
        (rootsGroupMap i (commAlgIdealTameOrder A B Q hQ)).hom'.toFun
          ((commAlgCanonicalTameCharacter A B Q hQ).toFun (r σ))).val.val := rfl

def

commAlgInertiaCompositeLocalRingHom

L51 ↗

EtaleFundamentalGroups.Inertia.commAlgInertiaCompositeLocalRingHom

Documentation

The actual local coefficient map at the precomposed inertia element, retained before any original field data enter the composite consumer.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification
universe u v w

Lean source · statement

def commAlgInertiaCompositeLocalRingHom
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B) [Q.IsPrime]
    {I : Type w} (r : I → commAlgIdealInertiaGroup A B Q) (σ : I) :
    Localization.AtPrime Q →+* Localization.AtPrime Q

theorem

commAlgInertiaCompositeLocalRingHom_comp_coefficient

L60 ↗

EtaleFundamentalGroups.Inertia.commAlgInertiaCompositeLocalRingHom_comp_coefficient

Documentation

Precomposition retains the actual coefficient square, with no automorphism action or local-inertia carrier exposed to the consumer.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification
universe u v w

Lean source · statement

theorem commAlgInertiaCompositeLocalRingHom_comp_coefficient
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B) [Q.IsPrime]
    {I : Type w} (r : I → commAlgIdealInertiaGroup A B Q) (σ : I) :
    (commAlgInertiaCompositeLocalRingHom A B Q r σ).comp
        (algebraMap B (Localization.AtPrime Q)) =
      (algebraMap B (Localization.AtPrime Q)).comp
        (commAlgIdealInertiaRingHom A B Q (r σ))

theorem

commAlgCanonicalTameCompositeValue_exists_coefficient

L73 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameCompositeValue_exists_coefficient

Documentation

The SAME full composite evaluates at an actual local coefficient ratio. The unit and ratio equation are produced, not assumed; the exponent is the actual original ramification index divided by the intrinsic tame order.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open RamificationTheory.HilbertRamification
universe u v w

Lean source · statement

theorem commAlgCanonicalTameCompositeValue_exists_coefficient
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
    {I : Type w} (r : I → commAlgIdealInertiaGroup A B Q)
    {k : Type v} [CommRing k] (i : Q.ResidueField →+* k)
    (π : Localization.AtPrime Q) (hπ : Irreducible π) (σ : I) :
    ∃ c : Localization.AtPrime Q, IsUnit c ∧
      π * c = (commAlgInertiaCompositeLocalRingHom A B Q r σ).toFun π ∧
      commAlgCanonicalTameCompositeValue A B Q hQ r i σ =
        (i.toFun ((IsLocalRing.residue (Localization.AtPrime Q)).toFun c)) ^
          (Q.ramificationIdx A / commAlgIdealTameOrder A B Q hQ)

Module documentation

Scalar evaluation of tame character composites

Declarations

commAlgCanonicalTameCompositeValue

commAlgCanonicalTameCompositeValue_eq_projection

commAlgInertiaCompositeLocalRingHom

commAlgInertiaCompositeLocalRingHom_comp_coefficient

commAlgCanonicalTameCompositeValue_exists_coefficient