Some results on the ranks of subalgebras #
This file contains some results on the ranks of subalgebras,
which are corollaries of rank_mul_rank.
Since their proof essentially depends on the fact that a non-trivial commutative ring
satisfies strong rank condition, we put them into a separate file.
theorem
Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Subalgebra R S)
(B : Subalgebra R S)
[Module.Free R ↥A]
[Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)]
:
Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank ↥A ↥(Algebra.adjoin ↥A ↑B)
theorem
Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Subalgebra R S)
(B : Subalgebra R S)
[Module.Free R ↥A]
[Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)]
:
Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥A * Module.finrank ↥A ↥(Algebra.adjoin ↥A ↑B)
theorem
Subalgebra.finrank_left_dvd_finrank_sup_of_free
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Subalgebra R S)
(B : Subalgebra R S)
[Module.Free R ↥A]
[Module.Free ↥A ↥(Algebra.adjoin ↥A ↑B)]
:
Module.finrank R ↥A ∣ Module.finrank R ↥(A ⊔ B)
theorem
Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Subalgebra R S)
(B : Subalgebra R S)
[Module.Free R ↥B]
[Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)]
:
Module.rank R ↥(A ⊔ B) = Module.rank R ↥B * Module.rank ↥B ↥(Algebra.adjoin ↥B ↑A)
theorem
Subalgebra.finrank_sup_eq_finrank_right_mul_finrank_of_free
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Subalgebra R S)
(B : Subalgebra R S)
[Module.Free R ↥B]
[Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)]
:
Module.finrank R ↥(A ⊔ B) = Module.finrank R ↥B * Module.finrank ↥B ↥(Algebra.adjoin ↥B ↑A)
theorem
Subalgebra.finrank_right_dvd_finrank_sup_of_free
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
(A : Subalgebra R S)
(B : Subalgebra R S)
[Module.Free R ↥B]
[Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)]
:
Module.finrank R ↥B ∣ Module.finrank R ↥(A ⊔ B)