English
For an algebra hom f: A →ₐ[R] B and a subalgebra S ⊆ A, the pullback along f of the image equals the join of S with the subalgebra generated by f^{-1}({0}).
Русский
Для гомоморфизма f: A →ₐ[R] B и подалгебры S ⊆ A, обратное отображение образа равно сумме (объединению) S и подалгебры, порожденной f^{-1}({0}).
LaTeX
$$$ (\operatorname{Subalgebra.map} f\ S)\operatorname{comap} f = S \;⊔\; \operatorname{Algebra.adjoin}_{R}(f^{-1}(\{0\})) $$$
Lean4
theorem comap_map_eq (f : A →ₐ[R] B) (S : Subalgebra R A) : (S.map f).comap f = S ⊔ Algebra.adjoin R (f ⁻¹' {0}) :=
by
apply le_antisymm
· intro x hx
rw [mem_comap, mem_map] at hx
obtain ⟨y, hy, hxy⟩ := hx
replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]
exact Subalgebra.add_mem _ (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)
· rw [← map_le, Algebra.map_sup, f.map_adjoin]
apply le_of_eq
rw [sup_eq_left, Algebra.adjoin_le_iff]
exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (S.map f).zero_mem)
