English
Let R be a ring and G an R-module. If x and y are pseudoequal elements in the over-category of G, then the images of the associated morphisms to G have the same image: Im(x.hom) = Im(y.hom).
Русский
Пусть R — кольцо, G — модуль над R. Если x и y псевдоравны в отношении к G, то образы соответствующих отображений в G совпадают: Im(x.hom) = Im(y.hom).
LaTeX
$$$\\operatorname{Im}(x_{\\mathrm{hom}}) = \\operatorname{Im}(y_{\\mathrm{hom}})$$$
Lean4
/-- In the category `Module R`, if `x` and `y` are pseudoequal, then the range of the associated
morphisms is the same. -/
theorem eq_range_of_pseudoequal {R : Type*} [Ring R] {G : ModuleCat R} {x y : Over G} (h : PseudoEqual G x y) :
LinearMap.range x.hom.hom = LinearMap.range y.hom.hom :=
by
obtain ⟨P, p, q, hp, hq, H⟩ := h
refine Submodule.ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
· obtain ⟨a', ha'⟩ := ha
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective p).1 hp a'
refine ⟨q a'', ?_⟩
dsimp at ha' ⊢
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, ← H, ModuleCat.hom_comp, LinearMap.comp_apply, ha'', ha']
· obtain ⟨a', ha'⟩ := ha
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a'
refine ⟨p a'', ?_⟩
dsimp at ha' ⊢
rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, H, ModuleCat.hom_comp, LinearMap.comp_apply, ha'', ha']
