Module docstring
{"# Some results on dimensions of algebra adjoin
This file contains some results on dimensions of Algebra.adjoin.
"}
Subalgebra.rank_sup_le_of_free
theorem
: Module.rank R ↥(A ⊔ B) ≤ Module.rank R A * Module.rank R B
Full source
/-- If `A` and `B` are subalgebras of a commutative `R`-algebra `S`, both of them are
free `R`-algebras, then the rank of the rank of the subalgebra generated by `A` and `B`
over `R` is less than or equal to the product of that of `A` and `B`. -/
theorem rank_sup_le_of_free : Module.rank R ↥(A ⊔ B) ≤ Module.rank R A * Module.rank R B := by
obtain ⟨ιA, bA⟩ := Free.exists_basis (R := R) (M := A)
obtain ⟨ιB, bB⟩ := Free.exists_basis (R := R) (M := B)
have h := Algebra.adjoin_union_coe_submodule R (A : Set S) (B : Set S)
rw [A.adjoin_eq_span_basis R bA, B.adjoin_eq_span_basis R bB, ← Algebra.sup_def,
Submodule.span_mul_span] at h
change Module.rank R ↥(toSubmodule (A ⊔ B)) ≤ _
rw [h, ← bA.mk_eq_rank'', ← bB.mk_eq_rank'']
refine (rank_span_le _).trans Cardinal.mk_mul_le |>.trans ?_
gcongr <;> exact Cardinal.mk_range_leInformal description
Let $R$ be a commutative ring and $S$ an $R$-algebra. Let $A$ and $B$ be free subalgebras of $S$ over $R$. Then the rank of the subalgebra generated by $A$ and $B$ over $R$ is bounded above by the product of the ranks of $A$ and $B$ over $R$, i.e.,
\[
\text{rank}_R(A \sqcup B) \leq \text{rank}_R(A) \cdot \text{rank}_R(B).
\]
Subalgebra.finrank_sup_le_of_free
theorem
: finrank R ↥(A ⊔ B) ≤ finrank R A * finrank R B
Full source
/-- If `A` and `B` are subalgebras of a commutative `R`-algebra `S`, both of them are
free `R`-algebras, then the `Module.finrank` of the rank of the subalgebra generated by `A` and `B`
over `R` is less than or equal to the product of that of `A` and `B`. -/
theorem finrank_sup_le_of_free : finrank R ↥(A ⊔ B) ≤ finrank R A * finrank R B := by
by_cases h : Module.Finite R A ∧ Module.Finite R B
· obtain ⟨_, _⟩ := h
simpa only [map_mul] using Cardinal.toNat_le_toNat (A.rank_sup_le_of_free B)
(Cardinal.mul_lt_aleph0 (rank_lt_aleph0 R A) (rank_lt_aleph0 R B))
wlog hA : ¬ Module.Finite R A generalizing A B
· have := this B A (fun h' ↦ h h'.symm) (not_and.1 h (of_not_not hA))
rwa [sup_comm, mul_comm] at this
rw [← rank_lt_aleph0_iff, not_lt] at hA
have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
show toSubmodule A ≤ toSubmodule (A ⊔ B) by simp
rw [show finrank R A = 0 from Cardinal.toNat_apply_of_aleph0_le hA,
show finrank R ↥(A ⊔ B) = 0 from Cardinal.toNat_apply_of_aleph0_le (hA.trans this), zero_mul]Informal description
Let $R$ be a commutative ring and $S$ a commutative $R$-algebra. Let $A$ and $B$ be free subalgebras of $S$ over $R$. Then the finite rank of the subalgebra generated by $A$ and $B$ over $R$ is bounded above by the product of the finite ranks of $A$ and $B$ over $R$, i.e.,
\[
\text{finrank}_R(A \sqcup B) \leq \text{finrank}_R(A) \cdot \text{finrank}_R(B).
\]