Module

Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet

26 declarations indexed from sourceView source ↗

Module documentation

Algebra exists polynomial is Unit aeval imp etale level Set

Imports35

Mathlib.RingTheory.TensorProduct.Maps
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.RingTheory.TensorProduct.Quotient
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Ideal.Over
Mathlib.FieldTheory.PurelyInseparable.Basic
Mathlib.FieldTheory.SeparableClosure
Mathlib.LinearAlgebra.Dimension.Free
Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Mathlib.LinearAlgebra.Dimension.Finite
Mathlib.RingTheory.Kaehler.TensorProduct
Mathlib.RingTheory.Kaehler.Basic
Mathlib.RingTheory.Unramified.Field
Mathlib.RingTheory.Unramified.Basic
Mathlib.RingTheory.Smooth.Fiber
Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.LocalRing.ResidueField.Basic
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.FiniteStability
Mathlib.RingTheory.FiniteType
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Finiteness.Defs
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.RingTheory.IsTensorProduct
Mathlib.RingTheory.Localization.BaseChange
Mathlib.Algebra.Module.LocalizedModule.Basic
Mathlib.RingTheory.Localization.Defs
Mathlib.FieldTheory.RatFunc.Basic
Mathlib.Algebra.Polynomial.Lifts
Mathlib.Algebra.Polynomial.Degree.Lemmas
Mathlib.Tactic.Choose

Imported by2

abbrev

rel

L72 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.rel

Documentation

The relation identifying the two images of the polynomial generator in the tensor product.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

abbrev rel : S ⊗[R] A

abbrev

LS

L76 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.LS

Documentation

The level-set algebra obtained by identifying the two polynomial-generator images.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

abbrev LS : Type u

def

toTensor

L80 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.toTensor

Documentation

The canonical map from the tensor product over the coefficient ring to the tensor product over its polynomial ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

def toTensor : S ⊗[R] A →ₐ[S] S ⊗[R[X]] A

theorem

toTensor_tmul

L85 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.toTensor_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

theorem toTensor_tmul (x : S) (a : A) : toTensor R S A (x ⊗ₜ[R] a) = x ⊗ₜ[R[X]] a

theorem

toTensor_rel

L89 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.toTensor_rel

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

theorem toTensor_rel : toTensor R S A (rel R S A) = 0

def

lsToTensor

L96 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.lsToTensor

Documentation

The quotient map identifying the level-set relation with the tensor product over the polynomial ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

def lsToTensor : LS R S A →ₐ[S] S ⊗[R[X]] A

theorem

lsToTensor_mk

L103 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.lsToTensor_mk

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

theorem lsToTensor_mk (x : S ⊗[R] A) :
    lsToTensor R S A (Ideal.Quotient.mk _ x) = toTensor R S A x

theorem

mk_algebraMap_tmul_one

L106 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.mk_algebraMap_tmul_one

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

theorem mk_algebraMap_tmul_one (p : R[X]) :
    (Ideal.Quotient.mk (Ideal.span {rel R S A}) (algebraMap R[X] S p ⊗ₜ[R] (1 : A)) : LS R S A)
      = Ideal.Quotient.mk (Ideal.span {rel R S A}) ((1 : S) ⊗ₜ[R] algebraMap R[X] A p)

def

inclA

L129 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.inclA

Documentation

The algebra map from the second factor to the level-set algebra over the polynomial ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

def inclA : A →ₐ[R[X]] LS R S A

theorem

inclA_apply

L137 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.inclA_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

theorem inclA_apply (a : A) : inclA R S A a = Ideal.Quotient.mk _ ((1 : S) ⊗ₜ[R] a)

def

tensorToLS

L141 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.tensorToLS

Documentation

The inverse map from the polynomial-ring tensor product to the level-set quotient.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

def tensorToLS : S ⊗[R[X]] A →ₐ[S] LS R S A

theorem

tensorToLS_tmul

L145 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.tensorToLS_tmul

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

theorem tensorToLS_tmul (x : S) (a : A) :
    tensorToLS R S A (x ⊗ₜ[R[X]] a) = Ideal.Quotient.mk _ (x ⊗ₜ[R] a)

def

lsEquiv

L155 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.lsEquiv

Documentation

The canonical equivalence between the level-set quotient and the tensor product over the polynomial ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

def lsEquiv : LS R S A ≃ₐ[S] S ⊗[R[X]] A

theorem

lsEquiv_mk

L167 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.lsEquiv_mk

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section LevelSet
variable (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
  [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A]
  [IsScalarTower R R[X] S] [IsScalarTower R R[X] A]

Lean source · statement

theorem lsEquiv_mk (x : S ⊗[R] A) : lsEquiv R S A (Ideal.Quotient.mk _ x) = toTensor
  R S A x

theorem

isSeparable_of_natCast_finrank_ne_zero

L174 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.isSeparable_of_natCast_finrank_ne_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Sep

Lean source · statement

theorem isSeparable_of_natCast_finrank_ne_zero (F E : Type u) [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E] (h : (Module.finrank F E : F) ≠ 0) : Algebra.IsSeparable F E

abbrev

algOfElt

L212 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.algOfElt

Documentation

The polynomial-ring algebra structure that sends the variable to the chosen element.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · statement

abbrev algOfElt (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (s : S) :
    Algebra R[X] S

theorem

isScalarTower_algOfElt

L215 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.isScalarTower_algOfElt

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · full declaration

theorem isScalarTower_algOfElt (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (s : S) :
    letI := algOfElt R S s; IsScalarTower R R[X] S :=
  letI := algOfElt R S s
  IsScalarTower.of_algebraMap_eq fun r => by
    change algebraMap R S r = (Polynomial.aeval s : R[X] →ₐ[R] S) (algebraMap R R[X] r)
    rw [AlgHom.commutes]

theorem

algebraMap_algOfElt_X

L222 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.algebraMap_algOfElt_X

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · full declaration

theorem algebraMap_algOfElt_X (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (s : S) :
    letI := algOfElt R S s; algebraMap R[X] S X = s := by
  change (Polynomial.aeval s : R[X] →ₐ[R] S) X = s
  exact Polynomial.aeval_X s

def

omegaEquiv

L231 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.omegaEquiv

Documentation

The base-change equivalence for the module of Kähler differentials.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core
section Omega
attribute [local instance] Algebra.TensorProduct.rightAlgebra

Lean source · statement

def omegaEquiv (P : Type u) [CommRing P] (A : Type u) [CommRing A] [Algebra P A]
    (S : Type u) [CommRing S] [Algebra P S] :
    S ⊗[P] Ω[A⁄P] ≃ₗ[S] Ω[(S ⊗[P] A)⁄S]

theorem

span_eq

L238 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.span_eq

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · statement

theorem span_eq (R : Type u) [CommRing R] (S : Type u) [CommRing S] (A : Type u) [CommRing A]
    [Algebra R S] [Algebra R A] [Algebra R[X] S] [Algebra R[X] A] (f : A) (s : S)
    (hf : algebraMap R[X] A X = f) (hs : algebraMap R[X] S X = s) :
    Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)} = Ideal.span {rel R S A}

theorem

subsingleton_tensor_of_smul_eq_zero

L244 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.subsingleton_tensor_of_smul_eq_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · statement

theorem subsingleton_tensor_of_smul_eq_zero {P : Type u} [CommRing P] {T : Type u} [Field T]
  [Algebra P T]
    {N : Type u} [AddCommGroup N] [Module P N] (q : P) (hq : algebraMap P T q ≠ 0)
    (hN : ∀ y : N, q • y = 0) : Subsingleton (T ⊗[P] N)

theorem

subsingleton_tensor_kaehler_of_isDomain

L261 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.subsingleton_tensor_kaehler_of_isDomain

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · statement

theorem subsingleton_tensor_kaehler_of_isDomain (P : Type u) [CommRing P] (A : Type u) [CommRing A]
    [Algebra P A] (K : Type u) [Field K] [Algebra P K]
    [IsDomain (K ⊗[P] A)] [Module.Finite K (K ⊗[P] A)]
    (h : (Module.finrank K (K ⊗[P] A) : K) ≠ 0) : Subsingleton (K ⊗[P] Ω[A⁄P])

theorem

exists_ne_zero_smul_baseChange_eq_zero

L273 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.exists_ne_zero_smul_baseChange_eq_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · statement

theorem exists_ne_zero_smul_baseChange_eq_zero (P : Type u) [CommRing P] (A : Type u) [CommRing A]
    [Algebra P A] (M : Type u) [AddCommGroup M] [Module P M] [Module A M] [IsScalarTower P A M]
    [Module.Finite A M]
    (Pk : Type u) [CommRing Pk] [IsDomain Pk] [Algebra P Pk] (K : Type u) [Field K] [Algebra Pk K]
    [IsFractionRing Pk K] [Algebra P K] [IsScalarTower P Pk K] [Subsingleton (K ⊗[P] M)] :
    ∃ D : Pk, D ≠ 0 ∧ ∀ y : Pk ⊗[P] M, D • y = 0

theorem

etale_baseChange_of_subsingleton

L319 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.etale_baseChange_of_subsingleton

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · statement

theorem etale_baseChange_of_subsingleton (P : Type u) [CommRing P] (A : Type u) [CommRing A]
    [Algebra P A] [Algebra.FinitePresentation P A]
    (S : Type u) [CommRing S] [IsLocalRing S] [Algebra P S]
    [Module.Finite S (S ⊗[P] A)] [Module.Free S (S ⊗[P] A)]
    (h : Subsingleton (IsLocalRing.ResidueField S ⊗[S] (S ⊗[P] Ω[A⁄P]))) :
    Algebra.Etale S (S ⊗[P] A)

theorem

core

L337 ↗

AlgebraicCurves.Foundations.Polynomial.Proofs.Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet.NoncritCore.core

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial
namespace NoncritCore
section Core

Lean source · statement

theorem core (R : Type u) [CommRing R] [IsLocalRing R]
    (A : Type u) [CommRing A] [Algebra R A] [Algebra.FinitePresentation R A]
    [IsDomain (IsLocalRing.ResidueField R ⊗[R] A)]
    (f : A) (m : ℕ) (hm : IsUnit (m : R))
    (hls : ∀ (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] (s : S),
        Module.Finite S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
        Module.Free S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
        Module.finrank S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) = m) :
    ∃ D : Polynomial R, (∃ i, IsUnit (D.coeff i)) ∧
      ∀ (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)] (s :
        S),
        IsUnit (Polynomial.aeval s D) →
        Algebra.Etale S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)})

theorem

exists_polynomial_isUnit_aeval_imp_etale_levelSet

L514 ↗

Algebra.exists_polynomial_isUnit_aeval_imp_etale_levelSet

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace Algebra_exists_polynomial_isUnit_aeval_imp_etale_levelSet
universe u
open scoped TensorProduct
open _root_.Polynomial

Lean source · statement

theorem _root_.Algebra.exists_polynomial_isUnit_aeval_imp_etale_levelSet
    (R : Type u) [CommRing R] [IsLocalRing R]
    (A : Type u) [CommRing A] [Algebra R A] [Algebra.FinitePresentation R A]
    [IsDomain (IsLocalRing.ResidueField R ⊗[R] A)]
    (f : A) (m : ℕ) (hm : IsUnit (m : R))
    (hls : ∀ (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] (s : S),
        Module.Finite S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
        Module.Free S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) ∧
        Module.finrank S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)}) = m) :
    ∃ D : Polynomial R, (∃ i, IsUnit (D.coeff i)) ∧
      ∀ (S : Type u) [CommRing S] [Algebra R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)] (s :
        S),
        IsUnit (Polynomial.aeval s D) →
        Algebra.Etale S (S ⊗[R] A ⧸ Ideal.span {(1 : S) ⊗ₜ[R] f - s ⊗ₜ[R] (1 : A)})

Module documentation

Algebra exists polynomial is Unit aeval imp etale level Set

Declarations