PushforwardRestrictionNatural.lean`

68 declarations, 0 contain sorry, 0 declared as axioms

Finite presentation of the associated sheaf of a finite module over a Noetherian ring.

def OAI.CoherentBaseChange.pushforwardRestrictNatIso line 10

Source documentation

The open basechange comparison is natural in the module sheaf.

def pushforwardRestrictNatIso {X Y : Scheme.{0}} (f : X ⟶ Y) (U : Y.Opens) :
    pushforward f ⋙ restrictFunctor U.ι ≅
      restrictFunctor (f ⁻¹ᵁ U).ι ⋙ pushforward (f ∣_ U) := by
…

lemma OAI.CoherentGlobal.exact_pushforward_iso line 33

lemma OAI.CoherentGlobal.exact_pushforward_affine line 43

Source documentation

Exactness of affine pushforward on coherent sheaves, for affine schemes not assumed to be definitionally spectra.

lemma exact_pushforward_affine {X Y : Scheme.{0}} [IsAffine X] [IsAffine Y]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [IsFinite f]
    (S : ShortComplex X.Modules)
    [S.X₁.IsFinitePresentation] [S.X₂.IsFinitePresentation] [S.X₃.IsFinitePresentation]
    (hS : S.Exact) : (S.map (pushforward f)).Exact := by
…

lemma OAI.CoherentGlobal.exact_pushforward line 76

Source documentation

Finite pushforward is exact on coherent sheaves, not on arbitrary sheaves.

lemma exact_pushforward {X Y : Scheme.{0}} [IsLocallyNoetherian Y]
    (f : X ⟶ Y) [IsFinite f] (S : ShortComplex X.Modules)
    [S.X₁.IsFinitePresentation] [S.X₂.IsFinitePresentation] [S.X₃.IsFinitePresentation]
    (hS : S.Exact) : (S.map (pushforward f)).Exact := by
…

abbrev OAI.CoherentGlobal.cohInclusion line 106
Source documentation
Inclusion of the coherent category into all structure-sheaf modules.
```
abbrev cohInclusion (X : Scheme.{0}) : Coh X ⥤ X.Modules :=
…
```
Mentions: OAI.CoherentGlobal.Coh
instance OAI.CoherentGlobal.cohInclusion_additive line 109
instance OAI.CoherentGlobal.cohInclusion_faithful line 112
instance OAI.CoherentGlobal.cohInclusion_kernels line 115
instance OAI.CoherentGlobal.cohInclusion_cokernels line 120
instance OAI.CoherentGlobal.cohInclusion_limits line 125
instance OAI.CoherentGlobal.cohInclusion_colimits line 129
def OAI.CoherentGlobal.cohPushforward line 134
Source documentation
Finite pushforward as a functor of coherent categories.
```
def cohPushforward {X Y : Scheme.{0}} [IsLocallyNoetherian Y]
    (f : X ⟶ Y) [IsFinite f] : Coh X ⥤ Coh Y :=
…
```
Mentions: OAI.CoherentGlobal.Coh
instance OAI.CoherentGlobal.cohPushforward_additive line 141
lemma OAI.CoherentGlobal.exact_cohPushforward line 148
instance OAI.CoherentGlobal.cohPushforward_preservesHomology line 158
instance OAI.CoherentGlobal.cohPushforward_preservesFiniteLimits line 163
instance OAI.CoherentGlobal.cohPushforward_preservesFiniteColimits line 168

lemma OAI.SheafTorsion.module_extension line 182

Source documentation

Torsion freedom is closed under left-exact module extensions.

lemma module_extension {R : Type u} [CommRing R]
    (S : ShortComplex (ModuleCat.{v} R)) (he : S.Exact) [Mono S.f]
    [Module.IsTorsionFree R S.X₁] [Module.IsTorsionFree R S.X₃] :
    Module.IsTorsionFree R S.X₂ where
…

lemma OAI.SheafTorsion.subobject line 203

Source documentation

Every section module of a module-sheaf subobject of a torsion-free sheaf is torsion-free. No local freeness is assumed.

lemma subobject {X : Scheme.{0}} {M N : X.Modules} (f : M ⟶ N) [Mono f]
    (hN : ∀ U, @Module.IsTorsionFree (X.sheaf.obj.obj U) (N.val.obj U) _ _
      (N.val.obj U).isModule)
    (U : X.Opensᵒᵖ) : @Module.IsTorsionFree (X.sheaf.obj.obj U) (M.val.obj U) _ _
      (M.val.obj U).isModule := by
…

lemma OAI.SheafTorsion.extension line 224

Source documentation

Sectionwise torsion freedom is closed under left-exact sheaf extensions: sections preserve the kernel, even though they need not preserve epimorphisms.

lemma extension {X : Scheme.{0}} (S : ShortComplex X.Modules)
    (he : S.Exact) [Mono S.f]
    (h₁ : ∀ U, @Module.IsTorsionFree (X.sheaf.obj.obj U) (S.X₁.val.obj U) _ _
      (S.X₁.val.obj U).isModule)
    (h₃ : ∀ U, @Module.IsTorsionFree (X.sheaf.obj.obj U) (S.X₃.val.obj U) _ _
      (S.X₃.val.obj U).isModule)
    (U : X.Opensᵒᵖ) : @Module.IsTorsionFree (X.sheaf.obj.obj U) (S.X₂.val.obj U) _ _
      (S.X₂.val.obj U).isModule := by
…

lemma OAI.SheafTorsion.coherent_extension line 245
def OAI.DualCartierRestriction.dualBaseChangeMap line 267
Source documentation
The canonical dual base-change map, without any false freeness assumption.
```
def dualBaseChangeMap (A : Type*) [CommRing A] [Algebra R A] :
    A ⊗[R] Module.Dual R M →ₗ[A] Module.Dual A (A ⊗[R] M) :=
…
```
lemma OAI.DualCartierRestriction.dualBaseChangeMap_tmul line 275
lemma OAI.DualCartierRestriction.quotient_one_tmul_surjective line 281
Source documentation
Scalar extension along a quotient is generated by tensors with first coordinate one, even when the module is not free.
```
lemma quotient_one_tmul_surjective (I : Ideal R) :
    Function.Surjective (fun m : M => (1 : R ⧸ I) ⊗ₜ[R] m) := by
…
```
lemma OAI.DualCartierRestriction.dualBaseChangeMap_injective line 290
Source documentation
Restriction of a dual to any effective principal Cartier divisor injects into the dual of the restricted module. The divisor need not be smooth for this algebraic assertion.
```
lemma dualBaseChangeMap_injective (t : R) (ht : IsSMulRegular R t) :
    Function.Injective (dualBaseChangeMap (R := R) (M := M) (R ⧸ Ideal.span ({t} : Set R))) := by
…
```
Mentions: OAI.DualCartierRestriction.dualBaseChangeMap
def OAI.CoherentDual.dualBaseChangeMorphism line 321
abbrev OAI.CoherentDual.principalQuotient line 334
abbrev OAI.CoherentDual.principalMap line 335
instance OAI.CoherentDual.principalTensor_finite line 337

def OAI.CoherentDual.principalDualInjection line 345

Source documentation

On an affine Cartier chart, the restriction of the sheaf dual embeds in the dual of the genuinely scalar-extended module.

def principalDualInjection :
    (Scheme.Modules.pullback (Spec.map (principalMap t))).obj
      (homSheaf (Spec A).sheaf (tilde M) (SheafOfModules.unit _)) ⟶
    homSheaf (Spec (principalQuotient t)).sheaf
      (tilde ((ModuleCat.extendScalars (principalMap t).hom).obj M))
      (SheafOfModules.unit _) :=
…

Mentions: OAI.CoherentDual.principalMap, OAI.CoherentDual.homSheaf, OAI.CoherentDual.principalQuotient

lemma OAI.CoherentDual.principalDualInjection_mono line 359

lemma OAI.CoherentDual.principalDual_restriction_torsionFree line 380

Source documentation

Restriction of a sheaf dual to an integral principal Cartier divisor is torsion-free.

lemma principalDual_restriction_torsionFree
    [(Ideal.span ({t} : Set A)).IsPrime]
    (U : (Spec (principalQuotient t)).Opensᵒᵖ) :
    @Module.IsTorsionFree ((Spec (principalQuotient t)).sheaf.obj.obj U)
      (((Scheme.Modules.pullback (Spec.map (principalMap t))).obj
        (homSheaf (Spec A).sheaf (tilde M) (SheafOfModules.unit _))).val.obj U) _ _
      ((((Scheme.Modules.pullback (Spec.map (principalMap t))).obj
        (homSheaf (Spec A).sheaf (tilde M) (SheafOfModules.unit _))).val.obj U).isModule) := by
…

Mentions: OAI.CoherentDual.principalQuotient, OAI.CoherentDual.principalMap, OAI.CoherentDual.homSheaf

lemma OAI.DualCartierRestriction.surjective_one_tmul line 403
Source documentation
Surjective scalar extension is generated by tensors with first coordinate one. No freeness, finite generation or chosen presentation is needed.
```
lemma surjective_one_tmul (h : Function.Surjective (algebraMap R A)) :
    Function.Surjective (fun m : M => (1 : A) ⊗ₜ[R] m) := by
…
```
lemma OAI.DualCartierRestriction.dualBaseChangeMap_injective_of_surjective line 421
Source documentation
Canonical dual specialization is injective for any surjective ring morphism whose kernel is generated by a regular element. This avoids identifying the target ring definitionally with a chosen quotient.
```
lemma dualBaseChangeMap_injective_of_surjective
    (h : Function.Surjective (algebraMap R A)) (t : R) (ht : IsSMulRegular R t)
    (hker : RingHom.ker (algebraMap R A) = Ideal.span ({t} : Set R)) :
    Function.Injective (dualBaseChangeMap (R := R) (M := M) A) := by
…
```
Mentions: OAI.DualCartierRestriction.dualBaseChangeMap
lemma OAI.CoherentAffine.isFinitePresentation_tilde line 459
lemma OAI.CoherentAffine.coherent_tilde line 482

def OAI.CoherentGlobal.restrictScalarsFullyFaithful line 496

Source documentation

Restriction along a quotient is fully faithful on modules.

def restrictScalarsFullyFaithful {A B : Type} [CommRing A] [CommRing B]
    (f : A →+* B) (hf : Function.Surjective f) :
    (ModuleCat.restrictScalars f).FullyFaithful where
…

lemma OAI.CoherentGlobal.affineGamma_injective line 508
lemma OAI.CoherentGlobal.affineGamma_surjective line 522
lemma OAI.CoherentGlobal.quasicoherent_pushforward_affine line 534

lemma OAI.CoherentGlobal.affinePushforward_full line 542

Source documentation

The sheaf pushforward under an affine closed immersion is full on quasicoherent sheaves, by the affine comparison.

lemma affinePushforward_full {A B : CommRingCat.{0}} (f : A ⟶ B)
    (hf : Function.Surjective f.hom) (M N : (Spec B).Modules)
    [M.IsQuasicoherent] [N.IsQuasicoherent] :
    Function.Surjective (fun g : M ⟶ N => (pushforward (Spec.map f)).map g) := by
…

def OAI.CoherentGlobal.cohTilde line 578
Source documentation
The associated sheaf functor on finite modules.
```
def cohTilde : FGModuleCat.{0} R ⥤ Coh (Spec R) :=
…
```
Mentions: OAI.CoherentGlobal.Coh
def OAI.CoherentGlobal.cohGamma line 584
Source documentation
Sections of a coherent sheaf on an affine Noetherian scheme form a finite module.
```
def cohGamma : Coh (Spec R) ⥤ FGModuleCat.{0} R :=
…
```
Mentions: OAI.CoherentGlobal.Coh
instance OAI.CoherentGlobal.cohTilde_faithful line 590
instance OAI.CoherentGlobal.cohTilde_full line 596
instance OAI.CoherentGlobal.cohTilde_essSurj line 602
instance OAI.CoherentGlobal.cohTilde_equivalence line 612
def OAI.CoherentGlobal.affineCohEquiv line 615
Source documentation
Affine coherent sheaves are genuinely equivalent to finite modules.
```
def affineCohEquiv : FGModuleCat.{0} R ≌ Coh (Spec R) := (cohTilde R).asEquivalence
```
Mentions: OAI.CoherentGlobal.Coh, OAI.CoherentGlobal.cohTilde
instance OAI.CoherentGlobal.cohTilde_additive line 617
abbrev OAI.CoherentDual.algebraSpecMap line 634
instance OAI.CoherentDual.algebraTensor_finite line 636

def OAI.CoherentDual.algebraDualInjection line 643

Source documentation

Canonical specialization into the dual over the target of a ring map.

def algebraDualInjection :
    (Scheme.Modules.pullback (algebraSpecMap φ)).obj
      (homSheaf (Spec A).sheaf (tilde M) (SheafOfModules.unit _)) ⟶
    homSheaf (Spec B).sheaf
      (tilde ((ModuleCat.extendScalars φ.hom).obj M))
      (SheafOfModules.unit _) := by
…

Mentions: OAI.CoherentDual.algebraSpecMap, OAI.CoherentDual.homSheaf

lemma OAI.CoherentDual.algebraDualInjection_mono line 657
lemma OAI.CoherentDual.tildeDual_algebra_restriction_torsionFree line 679

lemma OAI.CoherentDual.affineDual_algebra_restriction_torsionFree line 694

Source documentation

Specialization of a coherent sheaf dual to an integral Cartier quotient is torsion-free, using its finite module of sections.

lemma affineDual_algebra_restriction_torsionFree [IsDomain B]
    (N : (Spec A).Modules) [N.IsFinitePresentation]
    (h : Function.Surjective φ.hom) (t : A) (ht : IsSMulRegular A t)
    (hker : RingHom.ker φ.hom = Ideal.span ({t} : Set A))
    (U : (Spec B).Opensᵒᵖ) :
    @Module.IsTorsionFree ((Spec B).sheaf.obj.obj U)
      (((Scheme.Modules.pullback (algebraSpecMap φ)).obj
        (homSheaf (Spec A).sheaf N (SheafOfModules.unit _))).val.obj U) _ _
      ((((Scheme.Modules.pullback (algebraSpecMap φ)).obj
        (homSheaf (Spec A).sheaf N (SheafOfModules.unit _))).val.obj U).isModule) := by
…

Mentions: OAI.CoherentDual.algebraSpecMap, OAI.CoherentDual.homSheaf

def OAI.CoherentGlobal.closedLiftOpen line 724
Source documentation
The largest target open whose inverse image lies in a given source open.
```
def closedLiftOpen {X Y : Scheme.{0}} (f : X ⟶ Y) [IsClosedImmersion f]
    (U : X.Opens) : Y.Opens :=
…
```
lemma OAI.CoherentGlobal.preimage_closedLiftOpen line 728
lemma OAI.CoherentGlobal.le_closedLiftOpen_iff line 739

def OAI.CoherentGlobal.closedLiftFunctor line 752

Source documentation

The open-lift functor for a closed immersion.

def closedLiftFunctor {X Y : Scheme.{0}} (f : X ⟶ Y) [IsClosedImmersion f] :
    X.Opens ⥤ Y.Opens where
…

def OAI.CoherentGlobal.closedOpenAdjunction line 760
Source documentation
Inverse image of opens is a reflective localization for a closed embedding.
```
def closedOpenAdjunction {X Y : Scheme.{0}} (f : X ⟶ Y) [IsClosedImmersion f] :
    Opens.map f.base ⊣ closedLiftFunctor f where
…
```
Mentions: OAI.CoherentGlobal.closedLiftFunctor
instance OAI.CoherentGlobal.closedOpenCounitIso line 765

def OAI.CoherentGlobal.closedPresheafFullyFaithful line 773

Source documentation

Additive presheaves are recovered fully faithfully from their direct images.

def closedPresheafFullyFaithful {X Y : Scheme.{0}} (f : X ⟶ Y) [IsClosedImmersion f] :
    ((Functor.whiskeringLeft Y.Opensᵒᵖ X.Opensᵒᵖ AddCommGrpCat).obj
      (Opens.map f.base).op).FullyFaithful := by
…

instance OAI.CoherentGlobal.closedPushforward_faithful line 797

def OAI.CoherentGlobal.closedPushforwardPreimageAdd line 806

Source documentation

Underlying additive natural transformation of the descended map.

def closedPushforwardPreimageAdd {X Y : Scheme.{0}} (f : X ⟶ Y) [IsClosedImmersion f]
    {M N : X.Modules} (g : (pushforward f).obj M ⟶ (pushforward f).obj N) :
    M.presheaf ⟶ N.presheaf :=
…

lemma OAI.CoherentGlobal.closedPushforwardPreimageAdd_app line 811
lemma OAI.CoherentGlobal.closedPushforward_add_linear line 818
lemma OAI.CoherentGlobal.closedPushforward_full line 857
Source documentation
Pushforward under a closed immersion is full on all structure-sheaf modules. The underlying additive map is descended via the open adjunction; linearity is checked on inverse images of affine opens, where the structure ring homomorphism is surjective.
```
lemma closedPushforward_full {X Y : Scheme.{0}} (f : X ⟶ Y) [IsClosedImmersion f]
    (M N : X.Modules) :
    Function.Surjective (fun u : M ⟶ N => (pushforward f).map u) := by
…
```
instance OAI.CoherentGlobal.closedPushforward_full_instance line 869