Module

EtaleQuotientLift.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.EtaleQuotientLift

4 declarations indexed from sourceView source ↗

Module documentation

Lifting étale algebras through a surjective base map

For a surjective map R₀ → R and an étale R-algebra S, we construct an étale R₀-algebra whose base change is S. The construction uses mathlib's relative-dimension-zero submersive presentation, lifts its polynomial coefficients, and inverts the Jacobian of the resulting model.

The Jacobian maps to a unit in the original algebra, so this localization does not change the base change. Both the étale property and the algebra isomorphism are proved from the construction. No noetherian, field, or nilpotence hypothesis is used. This is the affine lifting step needed for comparing étale neighborhoods along a closed immersion.

Imports15

Nyll.SchemeTheory.RingTheory.JacobianLocalization
Mathlib.Algebra.Category.CommAlgCat.Basic
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.Group.Units.Equiv
Mathlib.Algebra.MvPolynomial.PDeriv
Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Mathlib.RingTheory.Extension.Generators
Mathlib.RingTheory.Extension.Presentation.Core
Mathlib.RingTheory.Extension.Presentation.Submersive
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.MvPolynomial.Tower
Mathlib.RingTheory.Smooth.StandardSmooth
Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Imported by3

lemma

tensorModel_jacobian

L60 ↗

Algebra.Etale.tensorModel_jacobian

Documentation

The Jacobian of the coefficient model becomes the original Jacobian after base change.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u₀ u v w t
open Algebra TensorProduct
namespace Algebra.Etale
variable {R : Type u} {S : Type v} {ι : Type w} {σ : Type t}
  [CommRing R] [CommRing S] [Algebra R S] [Finite σ]
  (P : PreSubmersivePresentation R S ι σ)
section Coefficients
variable (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S]
  [IsScalarTower R₀ R S] [P.HasCoeffs R₀]

Lean source · statement

lemma tensorModel_jacobian :
    P.tensorModelOfHasCoeffsEquiv R₀
      (1 ⊗ₜ[R₀] (P.ofHasCoeffs R₀).jacobian) = P.jacobian

def

tensorJacobianModelEquiv

L90 ↗

Algebra.Etale.tensorJacobianModelEquiv

Documentation

The coefficient model, localized at its Jacobian, still recovers the given algebra.

Source context 8 commands

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

@[expose] public section
noncomputable section
universe u₀ u v w t
open Algebra TensorProduct
namespace Algebra.Etale
variable {R : Type u} {S : Type v} {ι : Type w} {σ : Type t}
  [CommRing R] [CommRing S] [Algebra R S] [Finite σ]
  (P : PreSubmersivePresentation R S ι σ)
section Lift
variable (R₀ : Type*) [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S]
  [IsScalarTower R₀ R S] (Q : SubmersivePresentation R S ι σ)
  [Q.toPresentation.HasCoeffs R₀]

Lean source · statement

def tensorJacobianModelEquiv :
    R ⊗[R₀] Localization.Away (Q.toPreSubmersivePresentation.ofHasCoeffs R₀).jacobian ≃ₐ[R] S

lemma

exists_etale_lift_of_surjective

L108 ↗

Algebra.Etale.exists_etale_lift_of_surjective

Documentation

Every étale algebra over a quotient lifts to an étale algebra over the original ring.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u₀ u v w t
open Algebra TensorProduct
namespace Algebra.Etale
variable {R : Type u} {S : Type v} {ι : Type w} {σ : Type t}
  [CommRing R] [CommRing S] [Algebra R S] [Finite σ]
  (P : PreSubmersivePresentation R S ι σ)

Lean source · statement

lemma exists_etale_lift_of_surjective (R₀ : Type u₀) [CommRing R₀]
    [Algebra R₀ R]
    (h : Function.Surjective (algebraMap R₀ R)) [Algebra.Etale R S] :
    ∃ (T : Type u₀) (_ : CommRing T) (_ : Algebra R₀ T),
      Algebra.Etale R₀ T ∧ Nonempty (R ⊗[R₀] T ≃ₐ[R] S)

theorem

exists_etale_lift_of_quotient

L128 ↗

Algebra.Etale.exists_etale_lift_of_quotient

Documentation

Every étale algebra over an arbitrary quotient is the reduction of an étale algebra over the original ring. The constructed lift need not be finite as a module.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u₀ u v w t
open Algebra TensorProduct
namespace Algebra.Etale
variable {R : Type u} {S : Type v} {ι : Type w} {σ : Type t}
  [CommRing R] [CommRing S] [Algebra R S] [Finite σ]
  (P : PreSubmersivePresentation R S ι σ)

Lean source · statement

theorem exists_etale_lift_of_quotient
    {R A : Type u} [CommRing R] [CommRing A] (I : Ideal R)
    [Algebra (R ⧸ I) A] [Algebra.Etale (R ⧸ I) A] :
    ∃ C : CommAlgCat.{u} R, Algebra.Etale R C ∧
      Nonempty ((R ⧸ I) ⊗[R] C ≃ₐ[R ⧸ I] A)

Module documentation

Lifting étale algebras through a surjective base map

Declarations

tensorModel_jacobian

tensorJacobianModelEquiv

exists_etale_lift_of_surjective

exists_etale_lift_of_quotient