feat(algebra/algebra/subalgebra): subalgebra.map commutes with supr…

…emum (#10899)

This PR proves `(S ⊔ T).map f = S.map f ⊔ T.map f`.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/algebra/algebra/subalgebra.lean

@@ -540,6 +540,9 @@ lemma mul_mem_sup {S T : subalgebra R A} {x y : A} (hx : x ∈ S) (hy : y ∈ T)
   x * y ∈ S ⊔ T :=
 (S ⊔ T).mul_mem (mem_sup_left hx) (mem_sup_right hy)
 
+lemma map_sup (f : A →ₐ[R] B) (S T : subalgebra R A) : (S ⊔ T).map f = S.map f ⊔ T.map f :=
+(subalgebra.gc_map_comap f).l_sup
+
 @[simp, norm_cast]
 lemma coe_inf (S T : subalgebra R A) : (↑(S ⊓ T) : set A) = S ∩ T := rfl