Module

OriginalNormalizationResidueCoefficient.lean

Nyll.EtaleFundamentalGroups.Inertia.OriginalNormalizationResidueCoefficient

1 declaration indexed from sourceView source ↗

Module documentation

Coefficients of the original residue morphism

Identifies the original normalization residue morphism with the quotient map induced by its prescribed normalization coefficient action.

Imports7

Imported by3

theorem

originalNormalizationResidueMorphism_coefficientMap

L34 ↗

EtaleFundamentalGroups.Inertia.originalNormalizationResidueMorphism_coefficientMap

Documentation

The same original normalization residue morphism is the quotient of its prescribed normalization coefficient map. The original action is closed here.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationCommAlgGaloisAction

Lean source · statement

theorem originalNormalizationResidueMorphism_coefficientMap
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F))
    (d : normalizationDecompositionGroup A K F Q) :
    nativeAlgebraResidueCoefficientMap (normalizationCommAlgCat A F) Q
        ((normalizationResidueMorphism A K F Q).hom'.toFun d) =
      (Ideal.Quotient.mk Q).comp (normalizationGaloisRingHom A K F d.val)

Module documentation

Coefficients of the original residue morphism

Declarations

originalNormalizationResidueMorphism_coefficientMap