EtaleFundamentalGroups.Inertia.maximalQuotientResidueEquiv_localization_conjugate
The actual localization residue map is conjugate to its quotient map through the fixed canonical maximal-quotient equivalence.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe uLean source · statement
theorem maximalQuotientResidueEquiv_localization_conjugate
{B : Type u} [CommRing B] (Q : Ideal B) [Q.IsMaximal]
(e : B ≃+* B) (hQ : Q = Q.comap e.toRingHom) :
(IsLocalRing.ResidueField.mapEquiv
(Localization.localRingEquiv Q Q e hQ)).toRingHom =
((maximalQuotientResidueEquiv Q).toRingHom.comp
(Ideal.quotientEquiv Q Q e
((congrArg (Ideal.map e.toRingHom) hQ).trans
(Ideal.map_comap_eq_self_of_equiv e Q)).symm).toRingHom).comp
(maximalQuotientResidueEquiv Q).symm.toRingHom