Module

SeparableConstantsTensor.lean

Nyll.SchemeTheory.RingTheory.SeparableConstantsTensor

6 declarations indexed from sourceView source ↗

Module documentation

Tensor fields when separable constants lie in the base

If every element separable over the base in one field lies in the base image, that field is linearly disjoint from a separable extension. Their tensor product is therefore a field.

Imports6

Mathlib.FieldTheory.LinearDisjoint
Mathlib.FieldTheory.PrimitiveElement
Mathlib.FieldTheory.PurelyInseparable.Tower
Mathlib.RingTheory.Polynomial.GaussLemma
Mathlib.FieldTheory.AlgebraicClosure
Mathlib.RingTheory.Adjoin.PowerBasis

Imported by3

theorem

natDegree_minpoly_eq

L43 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range.P2mSepClosedTensorField.natDegree_minpoly_eq

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range
open Polynomial
open scoped TensorProduct IntermediateField
namespace P2mSepClosedTensorField
section Minpoly
variable {k F M : Type*} [Field k] [Field F] [Field M] [Algebra k F] [Algebra F M]
  [Algebra k M] [IsScalarTower k F M]

Lean source · statement

theorem natDegree_minpoly_eq (hsc : ∀ y : F, IsSeparable k y → y ∈ (algebraMap k F).range)
    {β : M} (hβ : IsSeparable k β) :
    (minpoly F β).natDegree = (minpoly k β).natDegree

theorem

hsc_range

L93 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range.P2mSepClosedTensorField.hsc_range

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range
open Polynomial
open scoped TensorProduct IntermediateField
namespace P2mSepClosedTensorField
section Overfield
variable {k F K Ω : Type*} [Field k] [Field F] [Field K] [Field Ω]
  [Algebra k F] [Algebra k K] [Algebra k Ω] (fa : F →ₐ[k] Ω) (fb : K →ₐ[k] Ω)

Lean source · statement

theorem hsc_range (hsc : ∀ y : F, IsSeparable k y → y ∈ (algebraMap k F).range)
    (y : fa.fieldRange) (hy : IsSeparable k y) : y ∈ (algebraMap k fa.fieldRange).range

theorem

linearDisjoint_adjoin_singleton

L104 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range.P2mSepClosedTensorField.linearDisjoint_adjoin_singleton

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range
open Polynomial
open scoped TensorProduct IntermediateField
namespace P2mSepClosedTensorField
section Overfield
variable {k F K Ω : Type*} [Field k] [Field F] [Field K] [Field Ω]
  [Algebra k F] [Algebra k K] [Algebra k Ω] (fa : F →ₐ[k] Ω) (fb : K →ₐ[k] Ω)

Lean source · statement

theorem linearDisjoint_adjoin_singleton
    (hsc : ∀ y : F, IsSeparable k y → y ∈ (algebraMap k F).range)
    {x : Ω} (hx : IsSeparable k x) :
    fa.fieldRange.toSubalgebra.LinearDisjoint (Algebra.adjoin k {x})

theorem

exists_le_adjoin_singleton

L126 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range.P2mSepClosedTensorField.exists_le_adjoin_singleton

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range
open Polynomial
open scoped TensorProduct IntermediateField
namespace P2mSepClosedTensorField
section Overfield
variable {k F K Ω : Type*} [Field k] [Field F] [Field K] [Field Ω]
  [Algebra k F] [Algebra k K] [Algebra k Ω] (fa : F →ₐ[k] Ω) (fb : K →ₐ[k] Ω)

Lean source · statement

theorem exists_le_adjoin_singleton [Algebra.IsSeparable k K]
    (B' : Subalgebra k Ω) (hB' : B' ≤ fb.range) [Module.Finite k B'] :
    ∃ β : K, B' ≤ Algebra.adjoin k {fb β}

theorem

linearDisjoint_range

L159 ↗

AlgebraicCurves.Foundations.FieldTheory.Proofs.Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range.P2mSepClosedTensorField.linearDisjoint_range

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range
open Polynomial
open scoped TensorProduct IntermediateField
namespace P2mSepClosedTensorField
section Overfield
variable {k F K Ω : Type*} [Field k] [Field F] [Field K] [Field Ω]
  [Algebra k F] [Algebra k K] [Algebra k Ω] (fa : F →ₐ[k] Ω) (fb : K →ₐ[k] Ω)

Lean source · statement

theorem linearDisjoint_range [Algebra.IsSeparable k K]
    (hsc : ∀ y : F, IsSeparable k y → y ∈ (algebraMap k F).range) :
    fa.fieldRange.toSubalgebra.LinearDisjoint fb.range

theorem

isField_of_isSeparable_of_forall_isSeparable_mem_range

L179 ↗

Algebra.TensorProduct.isField_of_isSeparable_of_forall_isSeparable_mem_range

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.FieldTheory.Proofs
namespace Algebra_TensorProduct_isField_of_isSeparable_of_forall_isSeparable_mem_range
open Polynomial
open scoped TensorProduct IntermediateField
universe u v w
open P2mSepClosedTensorField in

Lean source · statement

theorem _root_.Algebra.TensorProduct.isField_of_isSeparable_of_forall_isSeparable_mem_range
    (k : Type u) (F : Type v) (K : Type w) [Field k] [Field F] [Field K] [Algebra k F]
    [Algebra k K] [Algebra.IsSeparable k K]
    (hsc : ∀ y : F, IsSeparable k y → y ∈ (algebraMap k F).range) :
    IsField (F ⊗[k] K)

Module documentation

Tensor fields when separable constants lie in the base

Declarations

natDegree_minpoly_eq

hsc_range

linearDisjoint_adjoin_singleton

exists_le_adjoin_singleton

linearDisjoint_range

isField_of_isSeparable_of_forall_isSeparable_mem_range