of_isField' — Mathlib

English

Given an isDomain condition for a tensor product, there exists a field extension realizing linear disjointness.

Русский

При условии isDomain для тензорного произведения существует расширение поля, реализующее линейную несовпаденность.

LaTeX

$$$\exists K, fa, fb \; (fa.fieldRange.LinearDisjoint fb.fieldRange)$$$

Lean4

/-- If `A` and `B` are field extensions of `F`, such that `A ⊗[F] B` is a field, then for any
field extension of `F` that `A` and `B` embed into, their images are linearly disjoint. -/
theorem of_isField' {A : Type v} [Field A] {B : Type w} [Field B] [Algebra F A] [Algebra F B] (H : IsField (A ⊗[F] B))
    {K : Type*} [Field K] [Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K) :
    fa.fieldRange.LinearDisjoint fb.fieldRange :=
  by
  rw [linearDisjoint_iff']
  apply Subalgebra.LinearDisjoint.of_isField
  exact
    Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa fa.injective)
        (AlgEquiv.ofInjective fb fb.injective) |>.symm.toMulEquiv.isField
      H

Похожие утверждения