NYLL
Module

Algebra_isReduced_tensorProduct_of_perfectField.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_isReduced_tensorProduct_of_perfectField
7 declarations indexed from sourceView source ↗

Module documentation

Algebra is Reduced tensor Product of perfect Field

Imports4
  • Mathlib.FieldTheory.SeparablyGenerated
  • Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
  • Mathlib.RingTheory.TensorProduct.Pi
  • Mathlib.RingTheory.Unramified.Field
Imported by1

Declarations

theorem

isDomain_tensorProduct_of_isFractionRing

L35 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField.GredPerfect.isDomain_tensorProduct_of_isFractionRing
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField
open scoped TensorProduct
namespace GredPerfect
section PurelyTranscendental
variable {k : Type*} [Field k] {P E L : Type*} [CommRing P] [Algebra k P] [Field E] [Algebra k E]
  [Algebra P E] [IsScalarTower k P E] [IsFractionRing P E] [Field L] [Algebra k L]
Lean source · statement
theorem isDomain_tensorProduct_of_isFractionRing [IsDomain (P ⊗[k] L)] :
    IsDomain (E ⊗[k] L)
theorem

isDomain_adjoin_tensorProduct

L70 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField.GredPerfect.isDomain_adjoin_tensorProduct
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField
open scoped TensorProduct
namespace GredPerfect
Lean source · statement
theorem isDomain_adjoin_tensorProduct {k K L : Type*} [Field k] [Field K] [Algebra k K]
    [Field L] [Algebra k L] {ι : Type*} {v : ι → K} (hv : AlgebraicIndependent k v) :
    IsDomain ((IntermediateField.adjoin k (Set.range v)) ⊗[k] L)
theorem

isReduced_tensorProduct_of_formallyUnramified_of_isDomain

L84 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField.GredPerfect.isReduced_tensorProduct_of_formallyUnramified_of_isDomain
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField
open scoped TensorProduct
namespace GredPerfect
Lean source · statement
theorem isReduced_tensorProduct_of_formallyUnramified_of_isDomain
    (E K D : Type*) [Field E] [Field K] [Algebra E K] [Algebra.FormallyUnramified E K]
    [Algebra.EssFiniteType E K] [CommRing D] [Algebra E D] [IsDomain D] :
    IsReduced (K ⊗[E] D)
theorem

isReduced_tensorProduct_of_isSeparable_of_isDomain

L99 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField.GredPerfect.isReduced_tensorProduct_of_isSeparable_of_isDomain
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField
open scoped TensorProduct
namespace GredPerfect
Lean source · statement
theorem isReduced_tensorProduct_of_isSeparable_of_isDomain
    (k E K L : Type*) [Field k] [Field E] [Field K] [Field L] [Algebra k E] [Algebra k K]
    [Algebra E K] [IsScalarTower k E K] [Algebra k L] [Algebra.IsSeparable E K]
    [Algebra.EssFiniteType E K] [IsDomain (E ⊗[k] L)] :
    IsReduced (L ⊗[k] K)
theorem

isReduced_tensorProduct_field_of_essFiniteType

L113 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField.GredPerfect.isReduced_tensorProduct_field_of_essFiniteType
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField
open scoped TensorProduct
namespace GredPerfect
Lean source · statement
theorem isReduced_tensorProduct_field_of_essFiniteType
    (k K L : Type*) [Field k] [PerfectField k] [Field K] [Algebra k K]
    [Algebra.EssFiniteType k K] [Field L] [Algebra k L] :
    IsReduced (L ⊗[k] K)
theorem

isReduced_tensorProduct_of_finiteType

L127 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField.GredPerfect.isReduced_tensorProduct_of_finiteType
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField
open scoped TensorProduct
namespace GredPerfect
Lean source · statement
theorem isReduced_tensorProduct_of_finiteType
    (k B L : Type*) [Field k] [PerfectField k] [CommRing B] [Algebra k B] [IsReduced B]
    [Algebra.FiniteType k B] [Field L] [Algebra k L] :
    IsReduced (L ⊗[k] B)
theorem

isReduced_tensorProduct_of_perfectField

L172 ↗
Algebra.isReduced_tensorProduct_of_perfectField
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isReduced_tensorProduct_of_perfectField
open scoped TensorProduct
open scoped TensorProduct
universe u v w
Lean source · statement
theorem _root_.Algebra.isReduced_tensorProduct_of_perfectField
    (k : Type u) [Field k] [PerfectField k] (A : Type v) [CommRing A] [Algebra k A] [IsReduced A]
    (L : Type w) [Field L] [Algebra k L] :
    IsReduced (L ⊗[k] A)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.