English
If A and B are free subalgebras over R, then the finitary rank of the subalgebra generated by A and B is at most the product of the ranks of A and B.
Русский
Если A и B — свободные подалгебры над R, то finrank(A ⊔ B) ≤ finrank(A)·finrank(B).
LaTeX
$$$\\operatorname{finrank}_R \\; \\bigl(A \\sqcup B\\bigr) \\leq \\operatorname{finrank}_R A \\cdot \\operatorname{finrank}_R B$$$
Lean4
/-- 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]
