Module

Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced

30 declarations indexed from sourceView source ↗

Module documentation

Algebra Tensor Product is Reduced of perfect Field of is Reduced

Imports12

Mathlib.FieldTheory.SeparablyGenerated
Mathlib.RingTheory.AlgebraicIndependent.Adjoin
Mathlib.RingTheory.Etale.Field
Mathlib.RingTheory.Unramified.Field
Mathlib.RingTheory.EssentialFiniteness
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.TensorProduct.MvPolynomial
Mathlib.RingTheory.TensorProduct.Pi
Mathlib.Tactic.Ring

Imported by2

theorem

isPrime_of_mem_minimalPrimes

L46 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isPrime_of_mem_minimalPrimes

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

theorem isPrime_of_mem_minimalPrimes {p : Ideal A} (hp : p ∈ minimalPrimes A) : p.IsPrime

theorem

sInf_minimalPrimes_eq_bot

L48 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.sInf_minimalPrimes_eq_bot

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

theorem sInf_minimalPrimes_eq_bot [IsReduced A] : sInf (minimalPrimes A) = (⊥ : Ideal A)

abbrev

MinP

L54 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.MinP

Documentation

The type of minimal prime ideals of the ring.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

abbrev MinP (A : Type u) [CommRing A] : Type u

instance

fintypeMinP

L56 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.fintypeMinP

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

instance fintypeMinP [IsNoetherianRing A] : Fintype (MinP A)

instance

isPrime_minP

L59 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isPrime_minP

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

instance isPrime_minP (p : MinP A) : (p.1).IsPrime

instance

isDomain_quot_minP

L60 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isDomain_quot_minP

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

instance isDomain_quot_minP (p : MinP A) : IsDomain (A ⧸ p.1)

def

toProd

L63 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.toProd

Documentation

The algebra map to the product of the fraction fields of the minimal-prime quotients.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

def toProd (k : Type v) [CommRing k] [Algebra k A] :
    A →ₐ[k] (∀ p : MinP A, FractionRing (A ⧸ p.1))

theorem

toProd_apply

L68 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.toProd_apply

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

theorem toProd_apply (k : Type v) [CommRing k] [Algebra k A] (a : A) (p : MinP A) :
    toProd k a p = algebraMap (A ⧸ p.1) (FractionRing (A ⧸ p.1)) (Ideal.Quotient.mk p.1 a)

theorem

toProd_injective

L71 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.toProd_injective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

theorem toProd_injective (k : Type v) [CommRing k] [Algebra k A] [IsReduced A] :
    Function.Injective (toProd (A := A) k)

theorem

isReduced_tensor_of_forall_minimalPrimes

L87 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isReduced_tensor_of_forall_minimalPrimes

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
namespace F1
variable {A : Type u} [CommRing A]

Lean source · statement

theorem isReduced_tensor_of_forall_minimalPrimes {k : Type v} [Field k] {A : Type u} [CommRing A]
  [Algebra k A]
    [IsNoetherianRing A] [IsReduced A] (K : Type w) [Field K] [Algebra k K]
    (h : ∀ p ∈ minimalPrimes A, IsReduced (K ⊗[k] FractionRing (A ⧸ p))) :
    IsReduced (K ⊗[k] A)

def

polyToE

L120 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.polyToE

Documentation

The polynomial map into the rational function field after extending the coefficient field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

def polyToE : MvPolynomial ι k →+* FractionRing (MvPolynomial ι K)

theorem

polyToE_injective

L124 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.polyToE_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

theorem polyToE_injective : Function.Injective (polyToE k K ι)

def

fracToE

L129 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.fracToE

Documentation

The induced map of rational function fields after extending coefficients.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

def fracToE : FractionRing (MvPolynomial ι k) →ₐ[k] FractionRing (MvPolynomial ι K)

theorem

fracToE_algebraMap

L141 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.fracToE_algebraMap

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

theorem fracToE_algebraMap (p : MvPolynomial ι k) :
    fracToE k K ι (algebraMap (MvPolynomial ι k) _ p) = polyToE k K ι p

def

liftFrac

L148 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.liftFrac

Documentation

The map from the scalar-extended rational function field to the larger rational function field.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

def liftFrac : K ⊗[k] FractionRing (MvPolynomial ι k) →ₐ[k] FractionRing
  (MvPolynomial ι K)

def

inclPoly

L154 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.inclPoly

Documentation

The map induced by including polynomials into their fraction field after scalar extension.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

def inclPoly : K ⊗[k] MvPolynomial ι k →ₐ[k] K ⊗[k] FractionRing (MvPolynomial ι k)

theorem

liftFrac_comp_inclPoly_apply

L157 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.liftFrac_comp_inclPoly_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

theorem liftFrac_comp_inclPoly_apply (w : K ⊗[k] MvPolynomial ι k) :
    liftFrac k K ι (inclPoly k K ι w) =
      algebraMap (MvPolynomial ι K) (FractionRing (MvPolynomial ι K))
        (MvPolynomial.algebraTensorAlgEquiv k K w)

theorem

liftFrac_inclPoly_injective

L170 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.liftFrac_inclPoly_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · full declaration

theorem liftFrac_inclPoly_injective : Function.Injective (fun w => liftFrac k K ι (inclPoly k K ι
  w)) := by
  intro w₁ w₂ h
  simp only [liftFrac_comp_inclPoly_apply] at h
  exact (MvPolynomial.algebraTensorAlgEquiv k K).injective
    (IsFractionRing.injective (MvPolynomial ι K) (FractionRing (MvPolynomial ι K)) h)

theorem

exists_denom

L177 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.exists_denom

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

theorem exists_denom (z : K ⊗[k] FractionRing (MvPolynomial ι k)) :
    ∃ s : MvPolynomial ι k, s ≠ 0 ∧ ∃ w : K ⊗[k] MvPolynomial ι k,
      ((1 : K) ⊗ₜ[k] algebraMap (MvPolynomial ι k) (FractionRing (MvPolynomial ι k)) s) * z =
        inclPoly k K ι w

theorem

liftFrac_injective

L207 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.liftFrac_injective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section DOM
variable (k : Type*) [Field k] (K : Type*) [Field K] [Algebra k K] (ι : Type*)

Lean source · statement

theorem liftFrac_injective : Function.Injective (liftFrac k K ι)

def

toEAlgHom

L239 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.toEAlgHom

Documentation

The embedding of the generated intermediate field into the larger rational function field.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
attribute [local instance] fintypeMinP
attribute [local instance] isPrime_minP
attribute [local instance] isDomain_quot_minP
section Interface
variable {k : Type*} [Field k] (K : Type*) [Field K] [Algebra k K] {L : Type*} [Field L] [Algebra k
  L]
  {ι : Type*} (x : ι → L) (hx : AlgebraicIndependent k x)

Lean source · statement

def toEAlgHom : ↥(IntermediateField.adjoin k (Set.range x)) →ₐ[k] FractionRing
  (MvPolynomial ι K)

def

toE

L245 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.toE

Documentation

The ring homomorphism underlying the embedding into the larger rational function field.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
attribute [local instance] fintypeMinP
attribute [local instance] isPrime_minP
attribute [local instance] isDomain_quot_minP
section Interface
variable {k : Type*} [Field k] (K : Type*) [Field K] [Algebra k K] {L : Type*} [Field L] [Algebra k
  L]
  {ι : Type*} (x : ι → L) (hx : AlgebraicIndependent k x)

Lean source · statement

def toE : ↥(IntermediateField.adjoin k (Set.range x)) →+* FractionRing (MvPolynomial
  ι K)

theorem

toE_algebraMap

L249 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.toE_algebraMap

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
attribute [local instance] fintypeMinP
attribute [local instance] isPrime_minP
attribute [local instance] isDomain_quot_minP
section Interface
variable {k : Type*} [Field k] (K : Type*) [Field K] [Algebra k K] {L : Type*} [Field L] [Algebra k
  L]
  {ι : Type*} (x : ι → L) (hx : AlgebraicIndependent k x)

Lean source · statement

theorem toE_algebraMap (c : k) :
    toE K x hx (algebraMap k _ c) = algebraMap k (FractionRing (MvPolynomial ι K)) c

theorem

injective_liftToE

L253 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.injective_liftToE

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
attribute [local instance] fintypeMinP
attribute [local instance] isPrime_minP
attribute [local instance] isDomain_quot_minP
section Interface
variable {k : Type*} [Field k] (K : Type*) [Field K] [Algebra k K] {L : Type*} [Field L] [Algebra k
  L]
  {ι : Type*} (x : ι → L) (hx : AlgebraicIndependent k x)

Lean source · full declaration

theorem injective_liftToE :
    Function.Injective (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom k K (FractionRing
      (MvPolynomial ι K)))
      (toEAlgHom K x hx) (fun _ _ => Commute.all _ _)) := by
  let e : K ⊗[k] ↥(IntermediateField.adjoin k (Set.range x)) ≃ₐ[k] K ⊗[k] FractionRing
    (MvPolynomial ι k) :=
    Algebra.TensorProduct.congr AlgEquiv.refl hx.aevalEquivField.symm
  have hfac : (Algebra.TensorProduct.lift (IsScalarTower.toAlgHom k K (FractionRing (MvPolynomial ι
    K)))
      (toEAlgHom K x hx) (fun _ _ => Commute.all _ _)) = (liftFrac k K ι).comp e.toAlgHom := by
    apply Algebra.TensorProduct.ext'
    intro a f
    simp [liftFrac, toEAlgHom, e]
  rw [hfac]
  exact (liftFrac_injective k K ι).comp e.injective

theorem

isReduced_tensor_of_isSeparable

L287 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isReduced_tensor_of_isSeparable

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section FieldCase

Lean source · statement

theorem isReduced_tensor_of_isSeparable (F E L : Type*) [Field F] [Field E] [Field L] [Algebra F E]
  [Algebra F L]
    [Algebra.IsSeparable F L] [Algebra.EssFiniteType F L] : IsReduced (L ⊗[F] E)

theorem

isReduced_tensor_of_injective

L297 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isReduced_tensor_of_injective

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section FieldCase

Lean source · full declaration

theorem isReduced_tensor_of_injective {k F K E L : Type*} [Field k] [Field F] [Field K] [Field E]
  [Field L]
    [Algebra k F] [Algebra k K] [Algebra k E] [Algebra F E] [Algebra K E] [IsScalarTower k F E]
      [IsScalarTower k K E]
    [Algebra k L] [Algebra F L] [IsScalarTower k F L] [Algebra.IsSeparable F L]
      [Algebra.EssFiniteType F L]
    (hψ : Function.Injective (Algebra.TensorProduct.lift (Algebra.ofId F E) (IsScalarTower.toAlgHom
      k K E)
      (fun _ _ => Commute.all _ _) : F ⊗[k] K →ₐ[F] E)) : IsReduced (K ⊗[k] L) := by
  have : IsReduced (L ⊗[F] E) := isReduced_tensor_of_isSeparable F E L
  set ψ : F ⊗[k] K →ₐ[F] E := Algebra.TensorProduct.lift (Algebra.ofId F E) (IsScalarTower.toAlgHom
    k K E)
      (fun _ _ => Commute.all _ _) with hψdef
  let φ : L ⊗[F] (F ⊗[k] K) →ₐ[F] L ⊗[F] E := Algebra.TensorProduct.map (AlgHom.id F L) ψ
  have hφ : Function.Injective φ :=
    Module.Flat.lTensor_preserves_injective_linearMap (M := L) ψ.toLinearMap hψ
  let e : K ⊗[k] L ≃ₐ[k] L ⊗[F] (F ⊗[k] K) :=
    (Algebra.TensorProduct.comm k K L).trans
      ((Algebra.TensorProduct.cancelBaseChange k F F L K).symm.restrictScalars k)
  exact isReduced_of_injective ((φ.restrictScalars k).comp e.toAlgHom) (hφ.comp e.injective)

theorem

isReduced_tensor_of_adjoin_of_isSeparable

L319 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isReduced_tensor_of_adjoin_of_isSeparable

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section FieldCase

Lean source · statement

theorem isReduced_tensor_of_adjoin_of_isSeparable {k : Type*} [Field k] (K : Type*) [Field K]
  [Algebra k K]
    {L : Type*} [Field L] [Algebra k L] {ι : Type*} (x : ι → L) (hx : AlgebraicIndependent k x)
    [Algebra.IsSeparable (IntermediateField.adjoin k (Set.range x)) L]
    [Algebra.EssFiniteType (IntermediateField.adjoin k (Set.range x)) L] : IsReduced (K ⊗[k] L)

theorem

isReduced_tensor_field_of_perfectField

L353 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.isReduced_tensor_field_of_perfectField

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
section FieldCase

Lean source · statement

theorem isReduced_tensor_field_of_perfectField {k : Type*} [Field k] [PerfectField k] (L : Type*)
  [Field L] [Algebra k L]
    [Algebra.EssFiniteType k L] (K : Type*) [Field K] [Algebra k K] : IsReduced (K ⊗[k] L)

theorem

main

L371 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced.F1.main

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
namespace F1
attribute [local instance] fintypeMinP
attribute [local instance] isPrime_minP
attribute [local instance] isDomain_quot_minP

Lean source · statement

theorem main (k : Type*) [Field k] [PerfectField k] (A : Type*) [CommRing A] [Algebra k A]
  [Algebra.FiniteType k A]
    [IsReduced A] (K : Type*) [Field K] [Algebra k K] : IsReduced (K ⊗[k] A)

theorem

isReduced_of_perfectField_of_isReduced

L391 ↗

Algebra.TensorProduct.isReduced_of_perfectField_of_isReduced

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_TensorProduct_isReduced_of_perfectField_of_isReduced
open scoped TensorProduct
universe u v w
open TensorProduct
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP
attribute [local instance] F1.fintypeMinP
attribute [local instance] F1.isPrime_minP
attribute [local instance] F1.isDomain_quot_minP

Lean source · statement

theorem _root_.Algebra.TensorProduct.isReduced_of_perfectField_of_isReduced
    (k : Type u) [Field k] [PerfectField k] (A : Type v) [CommRing A] [Algebra k A]
      [Algebra.FiniteType k A] [IsReduced A]
    (K : Type w) [Field K] [Algebra k K] :
    IsReduced (K ⊗[k] A)

Module documentation

Algebra Tensor Product is Reduced of perfect Field of is Reduced

Declarations