Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebra/algebra/subalgebra): subalgebra.map commutes with supremum #10899

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat(algebra/algebra/subalgebra): subalgebra.map commutes with supremum #10899

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b63974d
lemma
tb65536 Dec 19, 2021
ce55030
review
tb65536 Dec 19, 2021
cb34f97
Update src/algebra/algebra/subalgebra.lean
tb65536 Dec 19, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions src/algebra/algebra/subalgebra.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
tb65536 marked this conversation as resolved.
Show resolved Hide resolved
(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

Expand Down