EtaleFundamentalGroups.Inertia.residueMap_coefficient_naturality
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u vLean source · statement
theorem residueMap_coefficient_naturality
{B : Type u} {C : Type v} [CommRing B] [CommRing C]
(P : Ideal B) [P.IsMaximal] (Q : Ideal C) [Q.IsPrime]
(j : B →+* C) (hj : P = Q.comap j)
(s : B →+* B) (t : C →+* C)
(a : P.ResidueField →+* P.ResidueField)
(b : Q.ResidueField →+* Q.ResidueField)
(ha : ∀ x : B, a.toFun ((algebraMap B P.ResidueField).toFun x) =
(algebraMap B P.ResidueField).toFun (s.toFun x))
(hb : ∀ x : C, b.toFun ((algebraMap C Q.ResidueField).toFun x) =
(algebraMap C Q.ResidueField).toFun (t.toFun x))
(hcomm : j.comp s = t.comp j) (x : P.ResidueField) :
(Ideal.ResidueField.map P Q j hj).toFun (a.toFun x) =
b.toFun ((Ideal.ResidueField.map P Q j hj).toFun x)