Finiteness results related to tensor products #
In this file we show that the supremum of two subalgebras that are finitely generated as modules, is again finitely generated.
theorem
Subalgebra.finite_sup
{K : Type u_1}
{L : Type u_2}
[CommSemiring K]
[CommSemiring L]
[Algebra K L]
(E1 E2 : Subalgebra K L)
[Module.Finite K ↥E1]
[Module.Finite K ↥E2]
:
Module.Finite K ↥(E1 ⊔ E2)
theorem
RingHom.surjective_of_tmul_eq_tmul_of_finite
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[Module.Finite R S]
(h₁ : ∀ (s : S), s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s)
:
Function.Surjective ⇑(algebraMap R S)