Module

FiniteIdealCanonicalTameScalarEvaluation.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteIdealCanonicalTameScalarEvaluation

3 declarations indexed from sourceView source ↗

Module documentation

Scalar evaluation at a finite ideal

Defines the canonical character scalar and localized inertia ring map. Produces a ratio unit giving both the local coefficient equation and scalar value.

Imports5

Imported by2

def

finiteIdealCanonicalTameScalar

L31 ↗

EtaleFundamentalGroups.Inertia.finiteIdealCanonicalTameScalar

Documentation

The scalar value of the existing canonical character, with its root and unit carriers closed inside this original ring-action owner.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification.DiscreteValuationRing
open scoped Pointwise
universe u v

Lean source · statement

def finiteIdealCanonicalTameScalar
    (A : Type u) (B G : Type v) [CommRing A] [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Group G] [Finite G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥) (σ : Q.inertia G) : Q.ResidueField

def

finiteIdealInertiaLocalRingHom

L40 ↗

EtaleFundamentalGroups.Inertia.finiteIdealInertiaLocalRingHom

Documentation

The existing prime-localization coefficient map at the actual inertia element. Only the literal local RingHom is returned.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification.DiscreteValuationRing
open scoped Pointwise
universe u v

Lean source · statement

def finiteIdealInertiaLocalRingHom
    (B G : Type v) [CommRing B] [Group G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (σ : Q.inertia G) :
    Localization.AtPrime Q →+* Localization.AtPrime Q

theorem

finiteIdealCanonicalTameScalar_exists_coefficient

L49 ↗

EtaleFundamentalGroups.Inertia.finiteIdealCanonicalTameScalar_exists_coefficient

Documentation

An actual ratio unit simultaneously supplies the local coefficient equation and the scalar evaluation of the SAME normalized character.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory RamificationTheory.HilbertRamification.DiscreteValuationRing
open scoped Pointwise
universe u v

Lean source · statement

theorem finiteIdealCanonicalTameScalar_exists_coefficient
    (A : Type u) (B G : Type v) [CommRing A] [CommRing B] [IsDedekindDomain B]
    [Algebra A B] [Group G] [Finite G] [MulSemiringAction G B]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
    (π : Localization.AtPrime Q) (hπ : Irreducible π) (σ : Q.inertia G) :
    ∃ c : Localization.AtPrime Q, IsUnit c ∧
      π * c = (finiteIdealInertiaLocalRingHom B G Q σ).toFun π ∧
      finiteIdealCanonicalTameScalar A B G Q hQ σ =
        ((IsLocalRing.residue (Localization.AtPrime Q)).toFun c) ^
          finiteIdealNormalizationExponent A B G Q hQ

Module documentation

Scalar evaluation at a finite ideal

Declarations

finiteIdealCanonicalTameScalar

finiteIdealInertiaLocalRingHom

finiteIdealCanonicalTameScalar_exists_coefficient