Module

NativeResidueRingAction.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeResidueRingAction

3 declarations indexed from sourceView source ↗

Module documentation

Coefficients of the native residue ring action

Forgetting coefficient linearity is a homomorphism. Transport through the fixed maximal-quotient equivalence preserves the literal coefficient equation.

Imports2

Imported by4

def

nativeAlgebraResidueRingEquivHom

L24 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueRingEquivHom

Documentation

The native quotient action, forgetting only coefficient linearity.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · full declaration

def nativeAlgebraResidueRingEquivHom
    {A : Type u} [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B.carrier) :
    (nativeAlgebraResidueAutomorphisms B Q).carrier →*
      ((B.carrier ⧸ Q) ≃+* (B.carrier ⧸ Q)) where
  toFun := nativeAlgebraResidueAutomorphismRingEquiv B Q
  map_one' := by
    apply RingEquiv.ext
    intro x
    rfl
  map_mul' σ τ := by
    apply RingEquiv.ext
    intro x
    rfl

def

nativeAlgebraResidueRingHom

L39 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueRingHom

Documentation

The SAME quotient action on the canonical localization residue field.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

def nativeAlgebraResidueRingHom
    {A : Type u} [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B.carrier) [Q.IsMaximal]
    (ρ : (nativeAlgebraResidueAutomorphisms B Q).carrier) :
    Q.ResidueField →+* Q.ResidueField

theorem

nativeAlgebraResidueRingHom_coefficient

L49 ↗

EtaleFundamentalGroups.Inertia.nativeAlgebraResidueRingHom_coefficient

Documentation

The coefficient formula survives the fixed quotient/residue transport.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v

Lean source · statement

theorem nativeAlgebraResidueRingHom_coefficient
    {A : Type u} [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B.carrier) [Q.IsMaximal]
    (ρ : (nativeAlgebraResidueAutomorphisms B Q).carrier)
    (s : B.carrier →+* B.carrier)
    (hs : nativeAlgebraResidueCoefficientMap B Q ρ = (Ideal.Quotient.mk Q).comp s)
    (b : B.carrier) :
    (nativeAlgebraResidueRingHom B Q ρ).toFun ((algebraMap B.carrier Q.ResidueField).toFun b) =
      (algebraMap B.carrier Q.ResidueField).toFun (s.toFun b)

Module documentation

Coefficients of the native residue ring action

Declarations

nativeAlgebraResidueRingEquivHom

nativeAlgebraResidueRingHom

nativeAlgebraResidueRingHom_coefficient