Commit 2024-12-20 20:23 75faccb7

feat: some more properties of linearly disjoint (#19614) Major new results:

• *.LinearDisjoint.map: linear disjointness is preserved by injective ring homomorphism.
• rank_sup_of_isAlgebraic -> rank_sup at the expense of importing AlgebraicIndependent.
• IntermediateField.LinearDisjoint.algEquiv_of_isAlgebraic: linear disjointness is preserved by isomorphisms, provided that one of the field is algebraic. Regarding https://mathoverflow.net/questions/8324:
• Subalgebra.LinearDisjoint.isDomain_of_injective, Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective: IntermediateField.LinearDisjoint.isDomain', IntermediateField.LinearDisjoint.exists_field_of_isDomain: under some flatness and injectivity conditions, if A and B are R-algebras (resp. fields), then A ⊗[R] B is a domain if and only if there exists a field such that A and B inject into it and their images are linearly disjoint.
• IntermediateField.LinearDisjoint.isField_of_forall, IntermediateField.LinearDisjoint.of_isField': if A and B are field extensions F, then A ⊗[F] B is a field if and only if for any field such that A and B map to it, their images are linearly disjoint.
• Algebra.TensorProduct.not_isField_of_transcendental, Algebra.TensorProduct.isAlgebraic_of_isField: if A and B are flat R-algebras, both of them are transcendental, then A ⊗[R] B cannot be a field, equivalently, if A ⊗[R] B is a field, then one of them is algebraic.
• Algebra.TensorProduct.isField_of_isAlgebraic: if E and K are field extensions of F, one of them is algebraic, such that E ⊗[F] K is a domain, then E ⊗[F] K is also a field.