English
A natural lifting formula for a morphism F from a direct limit to P is given by a unique lift identity along directed system maps.
Русский
Уникальное поднятие отображения через предел по направленной системе задаётся через соответствующее равенство композиции.
LaTeX
$$F x = lift L ι G f (fun i => F.comp (of L ι G f i)) (fun i j hij x => by rw [F.comp_apply, F.comp_apply, of_f]) x$$
Lean4
theorem sub_aux (f g : Hom P P') (x y) :
letI := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
f.toAlgHom (x * y) - g.toAlgHom (x * y) -
(P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) +
P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) ∈
P'.ker ^ 2 :=
by
letI := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
have :
(f.toAlgHom x - P'.σ (algebraMap P.Ring S' x)) * (f.toAlgHom y - g.toAlgHom y) +
(g.toAlgHom y - P'.σ (algebraMap P.Ring S' y)) * (f.toAlgHom x - g.toAlgHom x) ∈
P'.ker ^ 2 :=
by
rw [pow_two]
refine Ideal.add_mem _ (Ideal.mul_mem_mul ?_ ?_) (Ideal.mul_mem_mul ?_ ?_) <;>
simp only [RingHom.algebraMap_toAlgebra, RingHom.coe_comp, Function.comp_apply, ker, RingHom.mem_ker, map_sub,
algebraMap_toRingHom, algebraMap_σ, sub_self, toAlgHom_apply]
convert this using 1
simp only [map_mul]
ring
