Module

JacobianLocalization.lean

Nyll.SchemeTheory.RingTheory.JacobianLocalization

3 declarations indexed from sourceView source ↗

Module documentation

Localizing a presentation at its Jacobian

A presubmersive presentation has an injective assignment of relations to variables, without any assumption that its Jacobian is invertible. Composing with the presentation of the localization at that Jacobian gives a submersive presentation of the same relative dimension. In relative dimension zero the localized algebra is therefore étale.

Imports5

Mathlib.RingTheory.Extension.Presentation.Submersive
Mathlib.RingTheory.Extension.Presentation.Basic
Mathlib.RingTheory.Smooth.StandardSmooth
Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Mathlib.RingTheory.Localization.Away.Basic

Imported by2

def

jacobianLocalizationPresentation

L40 ↗

Algebra.PreSubmersivePresentation.jacobianLocalizationPresentation

Documentation

Inverting the Jacobian makes a presubmersive presentation submersive.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u v w t
open Algebra
namespace Algebra.PreSubmersivePresentation
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 · full declaration

def jacobianLocalizationPresentation :
    SubmersivePresentation R (Localization.Away P.jacobian) (Unit ⊕ ι) (Unit ⊕ σ) where
  toPreSubmersivePresentation :=
    (PreSubmersivePresentation.localizationAway (Localization.Away P.jacobian) P.jacobian).comp P
  jacobian_isUnit := by
    rw [PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian,
      PreSubmersivePresentation.localizationAway_jacobian, Algebra.smul_def]
    exact (IsLocalization.Away.algebraMap_isUnit P.jacobian).mul
      (IsLocalization.Away.algebraMap_isUnit P.jacobian)

lemma

jacobianLocalizationPresentation_dimension

L51 ↗

Algebra.PreSubmersivePresentation.jacobianLocalizationPresentation_dimension

Documentation

The Jacobian localization preserves the relative dimension of the presentation.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u v w t
open Algebra
namespace Algebra.PreSubmersivePresentation
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 jacobianLocalizationPresentation_dimension [Finite ι] :
    (jacobianLocalizationPresentation P).dimension = P.dimension

lemma

jacobianLocalization_etale

L61 ↗

Algebra.PreSubmersivePresentation.jacobianLocalization_etale

Documentation

A presentation of relative dimension zero becomes étale after inverting its Jacobian.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u v w t
open Algebra
namespace Algebra.PreSubmersivePresentation
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 jacobianLocalization_etale [Finite ι] (h : P.dimension = 0) :
    Algebra.Etale R (Localization.Away P.jacobian)

Module documentation

Localizing a presentation at its Jacobian

Declarations

jacobianLocalizationPresentation

jacobianLocalizationPresentation_dimension

jacobianLocalization_etale