Module

CommAlgCanonicalTameScalarEvaluation.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgCanonicalTameScalarEvaluation

5 declarations indexed from sourceView source ↗

Module documentation

Scalar values of intrinsic tame characters

Defines the scalar projection and local coefficient map of intrinsic inertia, and evaluates the canonical character using a uniformizer-ratio coefficient.

Imports7

Imported by2

def

commAlgCanonicalTameScalar

L32 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameScalar

Documentation

The scalar projection of the existing intrinsic canonical character.

Source context 5 commands

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

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

Lean source · statement

def commAlgCanonicalTameScalar
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
    (σ : commAlgIdealInertiaGroup A B Q) : Q.ResidueField

def

commAlgIdealInertiaLocalRingHom

L40 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealInertiaLocalRingHom

Documentation

The actual local coefficient map of an intrinsic inertia element.

Source context 5 commands

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

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

Lean source · statement

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

theorem

commAlgIdealInertiaLocalRingHom_comp_coefficient

L48 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealInertiaLocalRingHom_comp_coefficient

Documentation

The literal local RingHom has the prescribed value on every original coefficient, as a RingHom equation suitable for localization uniqueness.

Source context 5 commands

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

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

Lean source · statement

theorem commAlgIdealInertiaLocalRingHom_comp_coefficient
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B) [Q.IsPrime] (σ : commAlgIdealInertiaGroup A B Q) :
    (commAlgIdealInertiaLocalRingHom A B Q σ).comp
        (algebraMap B (Localization.AtPrime Q)) =
      (algebraMap B (Localization.AtPrime Q)).comp (commAlgIdealInertiaRingHom A B Q σ)

theorem

commAlgIdealInertiaLocalRingHom_eq_canonical

L61 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealInertiaLocalRingHom_eq_canonical

Documentation

The returned map is the literal inertia-localization map of the same coefficient automorphism, as verified on the original coefficients.

Source context 5 commands

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

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

Lean source · statement

theorem commAlgIdealInertiaLocalRingHom_eq_canonical
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B) [Q.IsPrime] (σ : commAlgIdealInertiaGroup A B Q) :
    commAlgIdealInertiaLocalRingHom A B Q σ =
      (inertiaLocalizationRingEquiv B Q σ.val.toRingEquiv σ.property).toRingHom

theorem

commAlgCanonicalTameScalar_exists_coefficient

L76 ↗

EtaleFundamentalGroups.Inertia.commAlgCanonicalTameScalar_exists_coefficient

Documentation

Scalar evaluation at an actual coefficient ratio, before an arbitrary source function or residue embedding is introduced. The result exposes no ambient automorphism group, local inertia group, or roots carrier.

Source context 5 commands

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

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

Lean source · statement

theorem commAlgCanonicalTameScalar_exists_coefficient
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    [IsDedekindDomain B] [Finite (B ≃ₐ[A] B)]
    (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥)
    (π : Localization.AtPrime Q) (hπ : Irreducible π)
    (σ : commAlgIdealInertiaGroup A B Q) :
    ∃ c : Localization.AtPrime Q, IsUnit c ∧
      π * c = (commAlgIdealInertiaLocalRingHom A B Q σ).toFun π ∧
      commAlgCanonicalTameScalar A B Q hQ σ =
        ((IsLocalRing.residue (Localization.AtPrime Q)).toFun c) ^
          (Q.ramificationIdx A / commAlgIdealTameOrder A B Q hQ)

Module documentation

Scalar values of intrinsic tame characters

Declarations

commAlgCanonicalTameScalar

commAlgIdealInertiaLocalRingHom

commAlgIdealInertiaLocalRingHom_comp_coefficient

commAlgIdealInertiaLocalRingHom_eq_canonical

commAlgCanonicalTameScalar_exists_coefficient