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 the 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 B : Subalgebra R S)
[Module.Free R ↥A]
[Module.Free ↥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 B : Subalgebra R S)
[Module.Free R ↥A]
[Module.Free ↥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 B : Subalgebra R S)
[Module.Free R ↥A]
[Module.Free ↥A ↥(Algebra.adjoin ↥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 B : Subalgebra R S)
[Module.Free R ↥B]
[Module.Free ↥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 B : Subalgebra R S)
[Module.Free R ↥B]
[Module.Free ↥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 B : Subalgebra R S)
[Module.Free R ↥B]
[Module.Free ↥B ↥(Algebra.adjoin ↥B ↑A)]
: