NYLL
Module

CommAlgStabilizerResidueCoefficients.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgStabilizerResidueCoefficients
2 declarations indexed from sourceView source ↗

Module documentation

Intrinsic stabilizer residue coefficients

The existing native intrinsic residue morphism has its actual algebra- automorphism coefficient formula after canonical localization transport.

Imports4
Imported by3

Declarations

def

commAlgDecompositionResidueRingHom

L26 ↗
EtaleFundamentalGroups.Inertia.commAlgDecompositionResidueRingHom
Documentation

The existing native decomposition carrier acts through its actual residue morphism.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
Lean source · statement
def commAlgDecompositionResidueRingHom
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B.carrier) [Q.IsMaximal]
    (d : (commAlgIdealDecompositionGroup A B Q).carrier) :
    Q.ResidueField →+* Q.ResidueField
theorem

commAlgStabilizerResidueRingHom_coefficient

L34 ↗
EtaleFundamentalGroups.Inertia.commAlgStabilizerResidueRingHom_coefficient
Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v
Lean source · statement
theorem commAlgStabilizerResidueRingHom_coefficient
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A)
    (Q : Ideal B.carrier) [Q.IsMaximal]
    (d : (commAlgIdealDecompositionGroup A B Q).carrier)
    (b : B.carrier) :
    (commAlgDecompositionResidueRingHom A B Q d).toFun
        ((algebraMap B.carrier Q.ResidueField).toFun b) =
      (algebraMap B.carrier Q.ResidueField).toFun
        ((commAlgAutomorphismRingHom A B d.val).toFun b)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.