From db1788c4538312e58da1c2b094bd869c2aeb6132 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Thu, 23 Dec 2021 14:26:39 +0000 Subject: [PATCH] feat(ring_theory/tensor_product): Supremum of finite dimensional subalgebras (#10922) The supremum of finite dimensional subalgebras is finite dimensional. --- src/ring_theory/tensor_product.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/ring_theory/tensor_product.lean b/src/ring_theory/tensor_product.lean index 1f2f521d593c5..2257a1b25af18 100644 --- a/src/ring_theory/tensor_product.lean +++ b/src/ring_theory/tensor_product.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison, Johan Commelin -/ -import linear_algebra.tensor_product +import linear_algebra.tensor_product_basis import ring_theory.adjoin.basic /-! @@ -789,3 +789,11 @@ by rw [product_map, alg_hom.range_comp, map_range, map_sup, ←alg_hom.range_com end end tensor_product end algebra + +lemma subalgebra.finite_dimensional_sup {K L : Type*} [field K] [comm_ring L] [algebra K L] + (E1 E2 : subalgebra K L) [finite_dimensional K E1] [finite_dimensional K E2] : + finite_dimensional K ↥(E1 ⊔ E2) := +begin + rw [←E1.range_val, ←E2.range_val, ←algebra.tensor_product.product_map_range], + exact (algebra.tensor_product.product_map E1.val E2.val).to_linear_map.finite_dimensional_range, +end