Nyll.SchemeTheory.RingTheory.Ramification.MaximalQuotientResidueNaturality

theorem

maximalQuotientResidueEquiv_naturality

EtaleFundamentalGroups.Inertia.maximalQuotientResidueEquiv_naturality

Documentation

The fixed canonical maximal-quotient residue equivalence intertwines the quotient and localization residue maps induced by the same automorphism. No residue action or comparison equation is supplied as an assumption.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u

Lean source · statement

theorem maximalQuotientResidueEquiv_naturality
    {B : Type u} [CommRing B] (Q : Ideal B) [Q.IsMaximal]
    (e : B ≃+* B) (hQ : Q = Q.comap e.toRingHom) (x : B ⧸ Q) :
    (IsLocalRing.ResidueField.mapEquiv
        (Localization.localRingEquiv Q Q e hQ)).toRingHom.toFun
        ((maximalQuotientResidueEquiv Q).toRingHom.toFun x) =
      (maximalQuotientResidueEquiv Q).toRingHom.toFun
        ((Ideal.quotientEquiv Q Q e
          ((congrArg (Ideal.map e.toRingHom) hQ).trans
            (Ideal.map_comap_eq_self_of_equiv e Q)).symm).toRingHom.toFun x)

MaximalQuotientResidueNaturality.lean

Module documentation

Naturality of the maximal-quotient residue equivalence

maximalQuotientResidueEquiv_naturality

Module documentation

Naturality of the maximal-quotient residue equivalence

Declarations

maximalQuotientResidueEquiv_naturality