English
A dual statement: swapping with maps f and g yields the same as swapping with swapped maps.
Русский
Двойное тождество: обмен с картами f,g эквивалентен обмену c поменянными картами.
LaTeX
$$$ (\\mathrm{comm}_{R} C D) \\circ (\\mathrm{map} f g) = (\\mathrm{map} g f) \\circ (\\mathrm{comm}_{R} A B).toAlgHom $$$
Lean4
theorem map_range (f : A →ₐ[R] C) (g : B →ₐ[R] D) :
(map f g).range = (includeLeft.comp f).range ⊔ (includeRight.comp g).range :=
by
apply le_antisymm
· rw [← map_top, ← adjoin_tmul_eq_top, ← adjoin_image, adjoin_le_iff]
rintro _ ⟨_, ⟨a, b, rfl⟩, rfl⟩
rw [map_tmul, ← mul_one (f a), ← one_mul (g b), ← tmul_mul_tmul]
exact mul_mem_sup (AlgHom.mem_range_self _ a) (AlgHom.mem_range_self _ b)
· rw [← map_comp_includeLeft f g, ← map_comp_includeRight f g]
exact sup_le (AlgHom.range_comp_le_range _ _) (AlgHom.range_comp_le_range _ _)
