Module

NativeAlgebraResidueCoefficient.lean

Nyll.SchemeTheory.RingTheory.Ramification.NativeAlgebraResidueCoefficient

4 declarations indexed from sourceView source ↗

Module documentation

Coefficient descriptions of algebra residue automorphisms

Defines ring equivalences and coefficient maps underlying algebra residue automorphisms. It proves that these coefficient maps determine the automorphisms and computes the residue morphism on coefficients.

Imports5

Imported by8

def

nativeAlgebraResidueAutomorphismRingEquiv

L30 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueAutomorphismRingEquiv

Documentation

Forget only coefficient-linearity in the actual native residue group.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v

Lean source · statement

def nativeAlgebraResidueAutomorphismRingEquiv
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A) (Q : Ideal R)
    (σ : nativeAlgebraResidueAutomorphisms R Q) : (R ⧸ Q) ≃+* (R ⧸ Q)

def

nativeAlgebraResidueCoefficientMap

L36 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueCoefficientMap

Documentation

The actual residue automorphism evaluated on original coefficients.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v

Lean source · statement

def nativeAlgebraResidueCoefficientMap
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A) (Q : Ideal R)
    (σ : nativeAlgebraResidueAutomorphisms R Q) : R →+* (R ⧸ Q)

theorem

nativeAlgebraResidueCoefficientMap_injective

L42 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueCoefficientMap_injective

Documentation

Original coefficients determine the native residue automorphism.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v

Lean source · statement

theorem nativeAlgebraResidueCoefficientMap_injective
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A) (Q : Ideal R) :
    Function.Injective (nativeAlgebraResidueCoefficientMap R Q)

theorem

nativeAlgebraResidueMorphism_coefficientMap

L53 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueMorphism_coefficientMap

Documentation

The same native residue morphism has its original coefficient formula.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v

Lean source · statement

theorem nativeAlgebraResidueMorphism_coefficientMap
    {A : Type u} [CommRing A] (R : CommAlgCat.{v} A)
    (G : Type v) [Group G] [MulSemiringAction G R]
    (Q : Ideal R)
    (hbase : ∀ g : G, (MulSemiringAction.toRingHom G R g).comp
      (commAlgCoefficientMap R) = commAlgCoefficientMap R)
    (d : nativeResidueStabilizer R G Q) :
    nativeAlgebraResidueCoefficientMap R Q
        ((nativeAlgebraResidueMorphism R G Q hbase).hom'.toFun d) =
      (Ideal.Quotient.mk Q).comp (stabilizerCoefficientRingEquiv R G Q d).toRingHom

Module documentation

Coefficient descriptions of algebra residue automorphisms

Declarations

nativeAlgebraResidueAutomorphismRingEquiv

nativeAlgebraResidueCoefficientMap

nativeAlgebraResidueCoefficientMap_injective

nativeAlgebraResidueMorphism_coefficientMap