CoherentClosedFunctor.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.CoherentGlobal.cohClosedPushforward_full line 9
instance OAI.CoherentGlobal.cohClosedPushforward_faithful line 16
def OAI.CoherentGlobal.cohClosedPushforwardFullyFaithful line 23
Source documentation
Fully faithful exact closed pushforward on coherent sheaves.
```
def cohClosedPushforwardFullyFaithful {X Y : Scheme.{0}} [IsLocallyNoetherian Y]
    (f : X ⟶ Y) [IsClosedImmersion f] : (cohPushforward f).FullyFaithful :=
…
```
Mentions: OAI.CoherentGlobal.cohPushforward

lemma OAI.CoherentGlobal.exists_principal_descent line 38

Source documentation

A coherent affine sheaf annihilated by a principal ideal descends to a coherent sheaf on the corresponding closed subscheme.

lemma exists_principal_descent (t : R) (M : (Spec R).Modules)
    [M.IsFinitePresentation]
    (h : Module.IsTorsionBy R (moduleSpecΓFunctor.obj M) t) :
    ∃ N : (Spec (CommRingCat.of (R ⧸ Ideal.span ({t} : Set R)))).Modules,
      N.IsFinitePresentation ∧ Nonempty
        ((pushforward (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk
          (Ideal.span ({t} : Set R)))))).obj N ≅ M) := by
…

lemma OAI.CoherentGlobal.exists_quotient_descent line 78

Source documentation

Descent for a coherent module along an affine quotient.

lemma exists_quotient_descent (I : Ideal R) (M : (Spec R).Modules)
    [M.IsFinitePresentation]
    (h : Module.IsTorsionBySet R (moduleSpecΓFunctor.obj M) I) :
    ∃ N : (Spec (CommRingCat.of (R ⧸ I))).Modules,
      N.IsFinitePresentation ∧ Nonempty
        ((pushforward (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))).obj N ≅ M) := by
…

lemma OAI.CoherentGlobal.exists_surjective_descent line 108

Source documentation

Descent along a surjective affine ring map, with annihilation of its kernel. The descended sheaf is a finite-module associated sheaf.

lemma exists_surjective_descent (f : R ⟶ S) (hf : Function.Surjective f.hom)
    (M : (Spec R).Modules) [M.IsFinitePresentation]
    (h : Module.IsTorsionBySet R (moduleSpecΓFunctor.obj M) (RingHom.ker f.hom)) :
    ∃ N : (Spec S).Modules, N.IsFinitePresentation ∧
      Nonempty ((pushforward (Spec.map f)).obj N ≅ M) := by
…

def OAI.CoherentGlobal.pushforwardIsoRoundtrip line 155

Source documentation

Pushforward around a scheme isomorphism.

def pushforwardIsoRoundtrip {X Y : Scheme.{0}} (e : X ≅ Y) :
    pushforward e.hom ⋙ pushforward e.inv ≅ 𝟭 X.Modules :=
…

lemma OAI.CoherentGlobal.exists_affine_closed_preimage line 161

Source documentation

Closed-support descent on affine schemes, without requiring them to be definitionally spectra. The hypothesis is annihilation by the kernel on the canonical affine chart of the target.

lemma exists_affine_closed_preimage {X Y : Scheme.{0}} [IsAffine Y]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [IsClosedImmersion f]
    (M : Y.Modules) [M.IsFinitePresentation]
    (h : Module.IsTorsionBySet Γ(Y, ⊤)
      (moduleSpecΓFunctor.obj ((pushforward Y.isoSpec.hom).obj M))
      (RingHom.ker f.appTop.hom)) :
    ∃ N : X.Modules, N.IsFinitePresentation ∧ Nonempty ((pushforward f).obj N ≅ M) := by
…

lemma OAI.BeckChevalleyUnit.isIso_other_mate line 198

Source documentation

The other mate of a square is invertible when its twice-adjoint comparison is invertible.

lemma isIso_other_mate (s : TwoSquare R₁ F₂ F₁ R₂)
    [IsIso ((mateEquiv a₄ a₃ s).natTrans)] :
    IsIso (((mateEquiv a₁ a₂).symm s).natTrans) := by
…

lemma OAI.BeckChevalleyUnit.map_unit_isIso line 213
Source documentation
Under an invertible base-change square and its invertible mate, the restricted original unit is invertible at every object at which the local unit is invertible. This is the local descent step for closed support.
```
lemma map_unit_isIso (s : TwoSquare R₁ F₂ F₁ R₂)
    [IsIso s.natTrans] [IsIso (((mateEquiv a₁ a₂).symm s).natTrans)]
    (M : A) [IsIso (a₂.unit.app (F₁.obj M))] : IsIso (F₁.map (a₁.unit.app M)) := by
…
```

def OAI.CoherentBaseChange.restrictSquare line 236

Source documentation

Open pushforward comparison viewed as a square of functors.

def restrictSquare : TwoSquare (pushforward f) (restrictFunctor (f ⁻¹ᵁ U).ι)
    (restrictFunctor U.ι) (pushforward (f ∣_ U)) :=
…

def OAI.CoherentBaseChange.rightSquare line 241
Source documentation
The twice-right-adjoint comparison of the open base-change square.
```
def rightSquare := mateEquiv (restrictAdjunction (f ⁻¹ᵁ U).ι)
…
```
def OAI.CoherentBaseChange.rightSquareIso line 246
Source documentation
Commutativity of the square gives an isomorphism of composite pushforwards, without base-change assumptions about quasicoherent sheaves.
```
def rightSquareIso : pushforward (f ⁻¹ᵁ U).ι ⋙ pushforward f ≅
    pushforward (f ∣_ U) ⋙ pushforward U.ι :=
…
```
lemma OAI.CoherentBaseChange.pushforwardRestrictNatIso_hom_app_app line 252
lemma OAI.CoherentBaseChange.rightSquare_eq line 256
instance OAI.CoherentBaseChange.rightSquare_natTrans_isIso line 279
instance OAI.CoherentBaseChange.pullbackSquare_natTrans_isIso line 283
def OAI.CoherentBaseChange.pullbackRestrictNatIso line 295
Source documentation
Pullback commutes with open restriction through the canonical mate, compatibly with the pullback-pushforward unit.
```
def pullbackRestrictNatIso : restrictFunctor U.ι ⋙ pullback (f ∣_ U) ≅
    pullback f ⋙ restrictFunctor (f ⁻¹ᵁ U).ι :=
…
```

lemma OAI.CoherentBaseChange.restrict_unit_isIso line 301

Source documentation

The restricted global unit is invertible whenever its local counterpart is.

lemma restrict_unit_isIso (M : Y.Modules)
    [IsIso ((pullbackPushforwardAdjunction (f ∣_ U)).unit.app
      ((restrictFunctor U.ι).obj M))] :
    IsIso ((restrictFunctor U.ι).map ((pullbackPushforwardAdjunction f).unit.app M)) := by
…

lemma OAI.CoherentGlobal.isIso_of_affine_restrict line 320
Source documentation
A morphism of scheme-module sheaves is invertible when its restrictions to all affine opens are invertible.
```
lemma isIso_of_affine_restrict {X : Scheme.{0}} {M N : X.Modules} (f : M ⟶ N)
    (h : ∀ U : X.affineOpens, IsIso ((restrictFunctor U.1.ι).map f)) : IsIso f := by
…
```

lemma OAI.SheafLocality.hom_ext_of_coversTop line 351

Source documentation

Equality of sheaf morphisms can be checked on any covering family.

lemma hom_ext_of_coversTop (hX : J.CoversTop X)
    {F G : Sheaf J A} {f g : F ⟶ G}
    (h : ∀ i, (J.overPullback A (X i)).map f = (J.overPullback A (X i)).map g) :
    f = g := by
…

lemma OAI.SheafLocality.mono_of_coversTop line 367

Source documentation

Monomorphism is local on a cover. No stalk-exactness assumption is used.

lemma mono_of_coversTop (hX : J.CoversTop X)
    {F G : Sheaf J A} (f : F ⟶ G)
    (h : ∀ i, Mono ((J.overPullback A (X i)).map f)) : Mono f := by
…

lemma OAI.SheafLocality.module_mono_of_coversTop line 379

Source documentation

The same descent statement for module sheaves.

lemma module_mono_of_coversTop (R : Sheaf J RingCat.{u}) (hX : J.CoversTop X)
    {F G : SheafOfModules.{u} R} (f : F ⟶ G)
    (h : ∀ i, Mono ((SheafOfModules.overFunctor R (X i)).map f)) : Mono f := by
…

lemma OAI.CoherentGlobal.hom_ext_of_open_cover line 403
Source documentation
Equality of scheme-module morphisms descends along an arbitrary open cover; affine charts are not required.
```
lemma hom_ext_of_open_cover {M N : X.Modules} {f g : M ⟶ N}
    (h : ∀ i, (restrictFunctor (U i).ι).map f = (restrictFunctor (U i).ι).map g) :
    f = g := by
…
```
lemma OAI.CoherentGlobal.isZero_of_open_cover line 425

lemma OAI.CoherentGlobal.isIso_of_open_cover line 433

Source documentation

Isomorphism of module sheaves is local on an open cover.

lemma isIso_of_open_cover {M N : X.Modules} (f : M ⟶ N)
    (h : ∀ i, IsIso ((restrictFunctor (U i).ι).map f)) : IsIso f := by
…

lemma OAI.CoherentGlobal.coherent_of_open_cover line 453
lemma OAI.CoherentGlobal.closedDescent_unit_isIso line 477
Source documentation
Membership in the essential image of closed pushforward is local on an open cover, with descent given by pullback.
```
lemma closedDescent_unit_isIso : IsIso ((pullbackPushforwardAdjunction f).unit.app M) := by
…
```
def OAI.CoherentGlobal.closedDescent_localIso line 486
Source documentation
Canonical local comparison of the descended module with its given closed-support representative.
```
def closedDescent_localIso (i : I) :
    (restrictFunctor (f ⁻¹ᵁ U i).ι).obj ((Scheme.Modules.pullback f).obj M) ≅ N i :=
…
```
lemma OAI.CoherentGlobal.preimage_cover line 494
lemma OAI.CoherentGlobal.closedDescent_coherent line 503
Source documentation
Pullback is coherent for objects which locally are coherent sheaves with closed support.
```
lemma closedDescent_coherent (hN : ∀ i, (N i).IsFinitePresentation) :
    ((Scheme.Modules.pullback f).obj M).IsFinitePresentation := by
…
```
lemma OAI.CoherentGlobal.exists_coherent_closed_preimage line 515
Source documentation
Descent in the coherent categories, with an pushforward isomorphism on the ambient scheme. This is the global closed-support step needed to put Cartier restriction and first Tor on the divisor.
```
lemma exists_coherent_closed_preimage [IsLocallyNoetherian Y] (hN : ∀ i, (N i).IsFinitePresentation) :
    ∃ Q : Coh X, Nonempty ((pushforward f).obj Q.obj ≅ M) := by
…
```
Mentions: OAI.CoherentGlobal.Coh
def OAI.ActualSheafTensor.tensorLeftIso line 534
Source documentation
An isomorphism of sheaves induces a natural tensor isomorphism.
```
def tensorLeftIso {M N : SheafOfModules.{u} (ringSheaf R)} (e : M ≅ N) :
    tensorLeft R M ≅ tensorLeft R N := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensorLeft
def OAI.ActualSheafTensor.tensorUnitLeftIso line 543
Source documentation
The tensor-with-unit functor is naturally the identity.
```
def tensorUnitLeftIso : tensorLeft R (SheafOfModules.unit _) ≅ 𝟭 _ := by
…
```
Mentions: OAI.ActualSheafTensor.tensorLeft
lemma OAI.ActualSheafTensor.tensorLeft_preservesMonomorphisms_of_unitIso line 554
Source documentation
Tensoring with the trivial line sheaf is exact by the tensor unit isomorphism.
```
lemma tensorLeft_preservesMonomorphisms_of_unitIso
    (M : SheafOfModules.{u} (ringSheaf R)) (e : M ≅ SheafOfModules.unit _) :
    (tensorLeft R M).PreservesMonomorphisms := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensorLeft
def OAI.ActualSheafTensor.tensorLeftMap line 573
Source documentation
Tensor a morphism of module sheaves on the left.
```
def tensorLeftMap {M N : SheafOfModules.{u} (ringSheaf R)} (f : M ⟶ N) :
    tensorLeft R M ⟶ tensorLeft R N := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensorLeft
def OAI.ActualSheafTensor.idealAction line 581
Source documentation
The multiplication morphism for a line ideal inside the structure sheaf. Its kernel and cokernel are the Cartier Tor and restriction objects.
```
def idealAction {L : SheafOfModules.{u} (ringSheaf R)}
    (i : L ⟶ SheafOfModules.unit _) : tensorLeft R L ⟶ 𝟭 _ :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensorLeft
def OAI.ActualSheafTensor.presheafOver line 600
Source documentation
Restriction of a module presheaf to the slice category.
```
def presheafOver : PresheafOfModules.{u} (ringSheaf R).obj ⥤
    PresheafOfModules.{u} (ringSheaf (R.over U)).obj :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf

def OAI.ActualSheafTensor.sheafifyOverMap line 605

Source documentation

The canonical comparison between sheafification and restriction.

def sheafifyOverMap (P : PresheafOfModules.{u} (ringSheaf R).obj) :
    (PresheafOfModules.sheafification (𝟙 (ringSheaf (R.over U)).obj)).obj
      ((presheafOver R U).obj P) ⟶
    ((PresheafOfModules.sheafification (𝟙 (ringSheaf R).obj)).obj P).over U :=
…

Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.presheafOver

lemma OAI.ActualSheafTensor.sheafifyOverMap_toSheaf line 615

Source documentation

The underlying comparison is the established sheafification comparison for a continuous cocontinuous functor.

lemma sheafifyOverMap_toSheaf (P : PresheafOfModules.{u} (ringSheaf R).obj) :
    (SheafOfModules.toSheaf _).map (sheafifyOverMap R U P) =
      ((Over.forget U).pushforwardContinuousSheafificationCompatibility AddCommGrpCat
        (J.over U) J).hom.app P.presheaf := by
…

Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.sheafifyOverMap

instance OAI.ActualSheafTensor.sheafifyOverMap_isIso line 626
theorem OAI.ActualSheafTensor.sheafifyOverMap_adjoint line 634
lemma OAI.ActualSheafTensor.sheafifyOverMap_naturality line 642

def OAI.ActualSheafTensor.sheafificationCompOver line 667

Source documentation

Sheafification and restriction are naturally isomorphic.

def sheafificationCompOver :
    presheafOver R U ⋙ PresheafOfModules.sheafification (𝟙 (ringSheaf (R.over U)).obj) ≅
      PresheafOfModules.sheafification (𝟙 (ringSheaf R).obj) ⋙
        SheafOfModules.overFunctor (ringSheaf R) U :=
…

Mentions: OAI.ActualSheafTensor.presheafOver, OAI.ActualSheafTensor.ringSheaf

def OAI.ActualSheafTensor.presheafTensorOverIso line 675
Source documentation
Tensor presheaves restrict objectwise exactly.
```
def presheafTensorOverIso (M N : PresheafOfModules.{u} (ringSheaf R).obj) :
    (presheafOver R U).obj (PresheafOfModulesOfCommRing.Monoidal.tensorObj (R := R.obj) M N) ≅
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.presheafOver
def OAI.ActualSheafTensor.tensorOverIso line 682
Source documentation
The tensor sheaf commutes with restriction to every slice site.
```
def tensorOverIso (M N : SheafOfModules.{u} (ringSheaf R)) :
    (tensor R M N).over U ≅ tensor (R.over U) (M.over U) (N.over U) :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensor

def OAI.ActualSheafTensor.presheafTensorCompOverIso line 691

Source documentation

Restriction commutes naturally with tensoring by a fixed presheaf.

def presheafTensorCompOverIso (M : PresheafOfModules.{u} (ringSheaf R).obj) :
    CategoryTheory.MonoidalCategory.tensorLeft
        (C := PresheafOfModules.{u} (R.obj ⋙ forget₂ CommRingCat RingCat)) M ⋙
…

Mentions: OAI.ActualSheafTensor.ringSheaf

def OAI.ActualSheafTensor.tensorLeftCompOverIso line 721
Source documentation
The restriction isomorphism for tensor sheaves is natural in the second variable. This is the exactness-descent bridge for Cartier twisting.
```
def tensorLeftCompOverIso (M : SheafOfModules.{u} (ringSheaf R)) :
    tensorLeft R M ⋙ SheafOfModules.overFunctor (ringSheaf R) U ≅
      SheafOfModules.overFunctor (ringSheaf R) U ⋙
        tensorLeft (R.over U) (M.over U) := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensorLeft

lemma OAI.ActualSheafTensor.idealAction_adjoint line 751

Source documentation

The ideal action is the adjoint of ordinary multiplication on pure tensors before sheafification.

lemma idealAction_adjoint {L : SheafOfModules.{u} (ringSheaf R)}
    (i : L ⟶ SheafOfModules.unit _) (M : SheafOfModules.{u} (ringSheaf R)) :
    (PresheafOfModules.sheafificationAdjunction (𝟙 (ringSheaf R).obj)).homEquiv _ _
      ((idealAction R i).app M) =
    (i.val ▷ M.val) ≫ (λ_ (M.val : PresheafOfModules (R.obj ⋙ forget₂ CommRingCat RingCat))).hom := by
…

Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.idealAction

lemma OAI.ActualSheafTensor.idealAction_pure line 768

Source documentation

Formula on pure tensors, including the sheafification unit.

lemma idealAction_pure {L : SheafOfModules.{u} (ringSheaf R)}
    (i : L ⟶ SheafOfModules.unit _) (M : SheafOfModules.{u} (ringSheaf R))
    (U : Cᵒᵖ) (l : L.val.obj U) (m : M.val.obj U) :
    ((idealAction R i).app M).val.app U
      (((PresheafOfModules.sheafificationAdjunction (𝟙 (ringSheaf R).obj)).unit.app
        (PresheafOfModulesOfCommRing.Monoidal.tensorObj (R := R.obj) L.val M.val)).app U
…

Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.idealAction

structure OAI.ActualSheafTensor.LineTrivialization line 794
Source documentation
Local trivializations of a rank-one locally free module sheaf.
```
structure LineTrivialization (M : SheafOfModules.{u} (ringSheaf R)) where
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf
lemma OAI.ActualSheafTensor.tensorLeft_preservesMonomorphisms_of_line line 802
Source documentation
Tensor by any line bundle preserves monomorphisms, by descent from the unit on its local trivializing cover.
```
lemma tensorLeft_preservesMonomorphisms_of_line
    (M : SheafOfModules.{u} (ringSheaf R)) (d : LineTrivialization R M) :
    (tensorLeft R M).PreservesMonomorphisms where
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.tensorLeft
lemma OAI.ActualSheafTensor.tensorLeft_preservesHomology_of_line line 835
Source documentation
Tensoring by a line bundle is actually exact throughout the category of module sheaves. Right exactness comes from the proved tensor-Hom adjunction.
```
lemma tensorLeft_preservesHomology_of_line
    (M : SheafOfModules.{u} (ringSheaf R)) (d : LineTrivialization R M) :
    (tensorLeft R M).PreservesHomology := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.tensorLeft