Commit 2024-11-27 08:55 7e86316a

View on Github →

feat(FieldTheory/LinearDisjoint): definition and basic properties of linearly disjoint of fields (#9651) This PR adds basics about the linearly disjoint fields. Main definitions:

  • IntermediateField.LinearDisjoint: an intermediate field A of E / F and an abstract field L between E / F are linearly disjoint over F, if they are linearly disjoint as subalgebras (Subalgebra.LinearDisjoint). Main results: Equivalent characterization of linearly disjointness:
  • IntermediateField.LinearDisjoint.linearIndependent_left: if A and L are linearly disjoint, then any F-linearly independent family on A remains linearly independent over L.
  • IntermediateField.LinearDisjoint.of_basis_left: conversely, if there exists an F-basis of A which remains linearly independent over L, then A and L are linearly disjoint.
  • IntermediateField.LinearDisjoint.linearIndependent_right: if A and L are linearly disjoint, then any F-linearly independent family on L remains linearly independent over A.
  • IntermediateField.LinearDisjoint.of_basis_right: conversely, if there exists an F-basis of L which remains linearly independent over A, then A and L are linearly disjoint.
  • IntermediateField.LinearDisjoint.linearIndependent_mul: if A and L are linearly disjoint, then for any family of F-linearly independent elements { a_i } of A, and any family of F-linearly independent elements { b_j } of L, the family { a_i * b_j } in S is also F-linearly independent.
  • IntermediateField.LinearDisjoint.of_basis_mul: conversely, if { a_i } is an F-basis of A, if { b_j } is an F-basis of L, such that the family { a_i * b_j } in E is F-linearly independent, then A and L are linearly disjoint. Other main results:
  • IntermediateField.LinearDisjoint.symm, IntermediateField.linearDisjoint_symm: linearly disjoint is symmetric.
  • IntermediateField.LinearDisjoint.rank_sup_of_isAlgebraic, IntermediateField.LinearDisjoint.finrank_sup: if A and B are linearly disjoint, then the rank of A ⊔ B is equal to the product of the rank of A and B. TODO: remove the algebraic assumptions (the proof becomes complicated).
  • IntermediateField.LinearDisjoint.of_finrank_sup: conversely, if A and B are finite extensions, such that rank of A ⊔ B is equal to the product of the rank of A and B, then A and B are linearly disjoint.
  • IntermediateField.LinearDisjoint.of_finrank_coprime: if the rank of A and B are coprime, then A and B are linearly disjoint.
  • IntermediateField.LinearDisjoint.inf_eq_bot: if A and B are linearly disjoint, then they are disjoint.

Estimated changes