Commit 2024-10-28 09:08 bacb7f7d

View on Github →

feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) (#17820) Main definitions:

  • Subalgebra.LinearDisjoint: two subalgebras are linearly disjoint, if they are linearly disjoint as submodules (Submodule.LinearDisjoint).
  • Subalgebra.LinearDisjoint.mulMap: if two subalgebras A and B of S / R are linearly disjoint, then there is A ⊗[R] B ≃ₐ[R] A ⊔ B induced by multiplication in S. Equivalent characterization of linearly disjointness:
  • Subalgebra.LinearDisjoint.linearIndependent_left_of_flat: if A and B are linearly disjoint, if B is a flat R-module, then for any family of R-linearly independent elements of A, they are also B-linearly independent.
  • Subalgebra.LinearDisjoint.of_basis_left: conversely, if a basis of A is also B-linearly independent, then A and B are linearly disjoint.
  • Subalgebra.LinearDisjoint.linearIndependent_right_of_flat: if A and B are linearly disjoint, if A is a flat R-module, then for any family of R-linearly independent elements of B, they are also A-linearly independent.
  • Subalgebra.LinearDisjoint.of_basis_right: conversely, if a basis of B is also A-linearly independent, then A and B are linearly disjoint.
  • Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat: if A and B are linearly disjoint, if one of A and B is flat, then for any family of R-linearly independent elements { a_i } of A, and any family of R-linearly independent elements { b_j } of B, the family { a_i * b_j } in S is also R-linearly independent.
  • Subalgebra.LinearDisjoint.of_basis_mul: conversely, if { a_i } is an R-basis of A, if { b_j } is an R-basis of B, such that the family { a_i * b_j } in S is R-linearly independent, then A and B are linearly disjoint. Other main results:
  • Subalgebra.LinearDisjoint.symm_of_commute, Subalgebra.linearDisjoint_symm_of_commute: linearly disjoint is symmetric under some commutative conditions.
  • Subalgebra.LinearDisjoint.bot_left, Subalgebra.LinearDisjoint.bot_right: the image of R in S is linearly disjoint with any other subalgebras.
  • Subalgebra.LinearDisjoint.sup_free_of_free: the compositum of two linearly disjoint subalgebras is a free module, if two subalgebras are also free modules.
  • Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, Subalgebra.LinearDisjoint.inf_eq_bot: if A and B are linearly disjoint, under suitable technical conditions, they are disjoint. The results with name containing "of_commute" also have corresponding specified versions assuming S is commutative.

Estimated changes