CotangentSheaf.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

The cotangent sheaf is the sheafification of the presheaf of Kähler differentials, with its universal derivation.

def OAI.ActualCotangent.constants line 14
Source documentation
Constants on every open come from the given structure morphism.
```
def constants : (Functor.const X.Opensᵒᵖ).obj (CommRingCat.of k) ⟶ X.presheaf where
…
```
def OAI.ActualCotangent.presheaf line 23
Source documentation
The presheaf of Kähler differentials of all section rings.
```
def presheaf : PresheafOfModules X.ringCatSheaf.obj :=
…
```
def OAI.ActualCotangent.sheaf line 27
Source documentation
The Zariski cotangent sheaf.
```
def sheaf : X.Modules :=
…
```
def OAI.ActualCotangent.derivation line 31
Source documentation
Its derivation is induced by the universal objectwise derivation.
```
def derivation : PresheafOfModulesOfCommRing.Derivation' ((sheaf f).val) (constants f) :=
…
```
Mentions: OAI.ActualCotangent.sheaf, OAI.ActualCotangent.constants
def OAI.ActualCotangent.homEquiv line 38
Source documentation
Universal property among sheaves of modules.
```
def homEquiv : (sheaf f ⟶ M) ≃ PresheafOfModulesOfCommRing.Derivation' (M.val) (constants f) :=
…
```
Mentions: OAI.ActualCotangent.sheaf, OAI.ActualCotangent.constants
lemma OAI.ActualCotangent.homEquiv_apply line 51
lemma OAI.ActualCotangent.constants_app line 68
lemma OAI.ActualCotangent.constants_app_apply line 77

def OAI.ActualCotangent.pushDerivation line 83

Source documentation

Push a derivation back through the map of section rings.

def pushDerivation (N : X.Modules)
    (D : PresheafOfModulesOfCommRing.Derivation' (N.val) (constants (f ≫ g))) :
    PresheafOfModulesOfCommRing.Derivation' (((Scheme.Modules.pushforward f).obj N).val) (constants g) where
…

Mentions: OAI.ActualCotangent.constants

lemma OAI.ActualCotangent.constants_appIso line 103
lemma OAI.ActualCotangent.constants_appIso_inv line 109

def OAI.ActualCotangent.restrictDerivation line 115

Source documentation

Restrict an sheaf derivation along an open immersion.

def restrictDerivation (M : Y.Modules) (D : PresheafOfModulesOfCommRing.Derivation' (M.val) (constants g)) :
    PresheafOfModulesOfCommRing.Derivation' ((M.restrict f).val) (constants (f ≫ g)) where
…

Mentions: OAI.ActualCotangent.constants

def OAI.ActualCotangent.pullDerivation line 137

Source documentation

Recover a derivation on an open scheme from one with values in its pushforward, using the restriction-pushforward counit.

def pullDerivation (N : X.Modules)
    (D : PresheafOfModulesOfCommRing.Derivation' (((Scheme.Modules.pushforward f).obj N).val) (constants g)) :
    PresheafOfModulesOfCommRing.Derivation' (N.val) (constants (f ≫ g)) :=
…

Mentions: OAI.ActualCotangent.constants

lemma OAI.ActualCotangent.pull_push line 143
lemma OAI.ActualCotangent.push_pull line 155

def OAI.ActualCotangent.openDerivationEquiv line 176

Source documentation

Derivations are local for open immersions.

def openDerivationEquiv (N : X.Modules) :
    PresheafOfModulesOfCommRing.Derivation' (((Scheme.Modules.pushforward f).obj N).val) (constants g) ≃
      PresheafOfModulesOfCommRing.Derivation' (N.val) (constants (f ≫ g)) where
…

Mentions: OAI.ActualCotangent.constants

def OAI.Derivation.extendEtale line 201
Source documentation
A derivation extends uniquely along any formally étale algebra.
```
def extendEtale (d : Derivation k R M) : Derivation k S M :=
…
```
lemma OAI.Derivation.extendEtale_algebraMap line 205
lemma OAI.Derivation.ext_of_algebraMap line 217

lemma OAI.Derivation.additive_ext_of_localization line 232

Source documentation

Additive Leibniz maps on a localization are determined on the base ring. This form does not prescribe a base-field scalar structure on the target.

lemma additive_ext_of_localization
    (A B : Type*) [CommRing A] [CommRing B] [Algebra A B]
    (T : Submonoid A) [IsLocalization T B]
    {N : Type*} [AddCommGroup N] [Module B N]
    (d e : B →+ N)
    (hd : ∀ a b : B, d (a*b) = a • d b + b • d a)
    (he : ∀ a b : B, e (a*b) = a • e b + b • e a)
    (h : ∀ a : A, d (algebraMap A B a) = e (algebraMap A B a)) : d = e := by
…

def OAI.AffineDerivation.sectionRestriction line 343
Source documentation
Restriction of sections regarded as a linear map over the base ring R.
```
def sectionRestriction {U V : (Spec (.of R)).Opens} (h : U ≤ V) :
    Γ(M,V) →ₗ[R] Γ(M,U) :=
…
```

def OAI.AffineDerivation.basic line 348

Source documentation

Derivations extend to the ring of sections of each principal open.

def basic (d : Derivation k R Γ(M,⊤)) (r : R) :
    Derivation k Γ(Spec (.of R), PrimeSpectrum.basicOpen r) Γ(M,PrimeSpectrum.basicOpen r) :=
…

lemma OAI.AffineDerivation.basic_algebraMap line 356

lemma OAI.AffineDerivation.basic_natural line 365

Source documentation

Compatibility of the extended derivations with restriction between basic opens.

lemma basic_natural (d : Derivation k R Γ(M,⊤)) (r s : R)
    (h : PrimeSpectrum.basicOpen s ≤ PrimeSpectrum.basicOpen r)
    (a : Γ(Spec (.of R), PrimeSpectrum.basicOpen r)) :
    sectionRestriction R M h (basic k R M d r a) =
      basic k R M d s (((Spec (.of R)).presheaf.map (homOfLE h).op) a) := by
…

Mentions: OAI.AffineDerivation.sectionRestriction, OAI.AffineDerivation.basic

def OAI.AffineDerivation.additive line 422
Source documentation
The compatible derivation on the basis extends as an additive map to all opens, using the sheaf condition of the target.
```
def additive (d : Derivation k R Γ(M,⊤)) :
    ((Spec (.of R)).ringCatSheaf.obj ⋙ forget₂ RingCat AddCommGrpCat) ⟶ M.presheaf :=
…
```
lemma OAI.AffineDerivation.additive_basic line 431
lemma OAI.AffineDerivation.additive_res line 439
lemma OAI.AffineDerivation.constants_spec_app line 446
lemma OAI.AffineDerivation.additive_mul line 456
lemma OAI.AffineDerivation.additive_algebraMap line 476

def OAI.AffineDerivation.derivation line 493

Source documentation

derivation of the structure sheaf extending the given affine coordinate derivation.

def derivation (d : Derivation k R Γ(M,⊤)) :
    PresheafOfModulesOfCommRing.Derivation' (M.val) (ActualCotangent.constants
      (Spec.map (CommRingCat.ofHom (algebraMap k R)))) where
…

Mentions: OAI.ActualCotangent.constants

lemma OAI.AffineDerivation.derivation_basic line 505
lemma OAI.AffineDerivation.derivation_top line 509
lemma OAI.AffineDerivation.global_leibniz line 524

def OAI.AffineDerivation.global line 533

Source documentation

Evaluate an sheaf derivation on the global coordinate functions.

def global (D : PresheafOfModulesOfCommRing.Derivation' (M.val) (ActualCotangent.constants
    (Spec.map (CommRingCat.ofHom (algebraMap k R))))) : Derivation k R Γ(M,⊤) where
…

Mentions: OAI.ActualCotangent.constants

lemma OAI.AffineDerivation.global_apply line 552
lemma OAI.AffineDerivation.global_derivation line 556
lemma OAI.AffineDerivation.derivation_global_basic line 561
lemma OAI.AffineDerivation.derivation_global line 581

def OAI.AffineDerivation.equiv line 596

Source documentation

Affine-coordinate derivations and sheaf derivations are equivalent.

def equiv : PresheafOfModulesOfCommRing.Derivation' (M.val) (ActualCotangent.constants
    (Spec.map (CommRingCat.ofHom (algebraMap k R)))) ≃ Derivation k R Γ(M,⊤) where
…

Mentions: OAI.ActualCotangent.constants

def OAI.ActualCotangent.affineHomEquiv line 635

Source documentation

The affine comparison on Hom sets, using sheaf derivations.

def affineHomEquiv (M : (Spec (.of R)).Modules) :
    (sheaf (Spec.map (CommRingCat.ofHom (algebraMap k R))) ⟶ M) ≃
      (tilde (ModuleCat.of R (KaehlerDifferential k R)) ⟶ M) :=
…

Mentions: OAI.ActualCotangent.sheaf

lemma OAI.ActualCotangent.affineHomEquiv_adjoint line 645
lemma OAI.ActualCotangent.affineHomEquiv_natural line 653
def OAI.ActualCotangent.affineIso line 683
Source documentation
The intrinsic cotangent sheaf of Spec R over k is the tilde sheaf of its Kähler module.
```
def affineIso : sheaf (Spec.map (CommRingCat.ofHom (algebraMap k R))) ≅
    tilde (ModuleCat.of R (KaehlerDifferential k R)) :=
…
```
Mentions: OAI.ActualCotangent.sheaf
lemma OAI.ActualCotangent.homEquiv_natural line 704
def OAI.ActualCotangent.openInverseHomEquiv line 710
Source documentation
The Hom-set version of the open cotangent comparison.
```
def openInverseHomEquiv (N : X.Modules) :
    (sheaf (f ≫ g) ⟶ N) ≃ ((sheaf g).restrict f ⟶ N) :=
…
```
Mentions: OAI.ActualCotangent.sheaf
lemma OAI.ActualCotangent.openInverseHomEquiv_eval line 716
lemma OAI.ActualCotangent.openInverseHomEquiv_natural line 725
def OAI.ActualCotangent.openIso line 745
Source documentation
The intrinsic cotangent sheaf is local for open immersions.
```
def openIso : (sheaf g).restrict f ≅ sheaf (f ≫ g) :=
…
```
Mentions: OAI.ActualCotangent.sheaf
abbrev OAI.ActualCotangent.affineModule line 756
Source documentation
The affine Kähler module, bundled before subsequent specialization.
```
abbrev affineModule := ModuleCat.of R (KaehlerDifferential k R)
```

def OAI.ActualCotangent.openAffineIso line 759

Source documentation

An open affine chart of any scheme computes its cotangent sheaf.

def openAffineIso (i : Spec (CommRingCat.of R) ⟶ Y) [IsOpenImmersion i]
    (h : i ≫ g = Spec.map (CommRingCat.ofHom (algebraMap k R))) :
    (sheaf g).restrict i ≅ tilde (ModuleCat.of R (KaehlerDifferential k R)) :=
…

Mentions: OAI.ActualCotangent.sheaf