CoherentGlobalDual.lean`

63 declarations, 0 contain sorry, 0 declared as axioms

Local linear Hom for sheaves of modules and coherence of duals on Noetherian schemes.

abbrev OAI.CoherentDual.LocalAddHom line 16
abbrev OAI.CoherentDual.localApp line 21
def OAI.CoherentDual.localSMul line 24
instance OAI.CoherentDual.localHomSMul line 40
lemma OAI.CoherentDual.local_smul_app line 44
lemma OAI.CoherentDual.local_add_app line 49
lemma OAI.CoherentDual.local_zero_app line 54
lemma OAI.CoherentDual.local_ext line 57
instance OAI.CoherentDual.localHomModule line 62
def OAI.CoherentDual.linearLocalHom line 71
Source documentation
Local morphisms that are linear for every local ring of sections.
```
def linearLocalHom (X : C) : Submodule (R.obj (op X)) (LocalAddHom R M N X) where
…
```
Mentions: OAI.CoherentDual.LocalAddHom
def OAI.CoherentDual.linearLocalSubfunctor line 86
Source documentation
Linearity is preserved by restricting local natural transformations.
```
def linearLocalSubfunctor : Subfunctor (presheafHom M.presheaf N.presheaf) where
…
```
def OAI.CoherentDual.homPresheaf line 93
Source documentation
The linear internal Hom presheaf, with its natural module structure.
```
def homPresheaf : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat) where
…
```
lemma OAI.CoherentDual.local_naturality line 124

theorem OAI.CoherentDual.linearLocalSubfunctor_isSheaf line 131

Source documentation

Pointwise local linearity is a sheaf-local condition.

theorem linearLocalSubfunctor_isSheaf {J : GrothendieckTopology C}
    (hN : Presheaf.IsSheaf J N.presheaf) :
    Presheaf.IsSheaf J (linearLocalSubfunctor (R := R) (M := M) (N := N)).toFunctor := by
…

Mentions: OAI.CoherentDual.linearLocalSubfunctor

lemma OAI.CoherentDual.homPresheaf_isSheaf line 165

def OAI.CoherentDual.homSheaf line 172

Source documentation

The actual sheaf of modules of local linear maps.

def homSheaf {J : GrothendieckTopology C} (R : Sheaf J CommRingCat.{max u v w})
    (M N : SheafOfModules.{max u v w z}
      ((sheafCompose J (forget₂ CommRingCat.{max u v w} RingCat.{max u v w})).obj R)) :
    SheafOfModules.{max u v w z}
      ((sheafCompose J (forget₂ CommRingCat.{max u v w} RingCat.{max u v w})).obj R) where
…

def OAI.CoherentDual.localHomEquiv line 183
Source documentation
Local linear transformations are exactly ordinary module morphisms on the slice site. This identifies the just-constructed sheaf with genuine internal Hom.
```
def localHomEquiv (X : C) :
    linearLocalHom (R := R) (M := M) (N := N) X ≃
…
```
Mentions: OAI.CoherentDual.linearLocalHom

def OAI.CoherentDual.homSheafSectionsEquiv line 202

Source documentation

Sections of homSheaf are the actual morphisms of the restricted sheaves.

def homSheafSectionsEquiv {J : GrothendieckTopology C}
    (R : Sheaf J CommRingCat.{max u v w})
    (M N : SheafOfModules.{max u v w z}
      ((sheafCompose J (forget₂ CommRingCat.{max u v w} RingCat.{max u v w})).obj R))
    (X : C) :
    (homSheaf R M N).val.obj (op X) ≃ (M.over X ⟶ N.over X) where
…

Mentions: OAI.CoherentDual.homSheaf

def OAI.CoherentDual.unitLocalMap line 226
def OAI.CoherentDual.unitLocalEquiv line 250
Source documentation
The expected free rank-one evaluation law, with the local ring action.
```
def unitLocalEquiv (X : C₀) :
    linearLocalHom (R := R₀) (M := PresheafOfModules.unit
…
```
Mentions: OAI.CoherentDual.linearLocalHom
def OAI.CoherentDual.unitHomPresheafIso line 294
Source documentation
Evaluation at one is an isomorphism of module presheaves, not just a bijection on global morphisms.
```
def unitHomPresheafIso :
    homPresheaf (R := R) (M := PresheafOfModules.unit
…
```
Mentions: OAI.CoherentDual.homPresheaf
def OAI.CoherentDual.unitHomSheafIso line 315
Source documentation
The genuine internal Hom from the structure sheaf is the target sheaf.
```
def unitHomSheafIso :
    homSheaf R₁ (SheafOfModules.unit _) N₁ ≅ N₁ :=
…
```
Mentions: OAI.CoherentDual.homSheaf
def OAI.CoherentDual.precompLocal line 330
Source documentation
Precomposition in the genuine module of local linear maps.
```
def precompLocal (f : M ⟶ M') (X : C) :
    linearLocalHom (R := R) (M := M') (N := N) X →ₗ[R.obj (op X)]
…
```
Mentions: OAI.CoherentDual.linearLocalHom
def OAI.CoherentDual.precompPresheaf line 350

def OAI.CoherentDual.homSheafFunctor line 365

Source documentation

Contravariant internal Hom into a fixed sheaf.

def homSheafFunctor : (SheafOfModules.{u} ((sheafCompose J (forget₂ CommRingCat RingCat)).obj R))ᵒᵖ ⥤ SheafOfModules.{u} ((sheafCompose J (forget₂ CommRingCat RingCat)).obj R) where
…

def OAI.CoherentDual.homSheafEvaluationIso line 388

Source documentation

Evaluation of internal Hom is the actual representable functor on the slice site. In particular no local presentation or exactness is postulated.

def homSheafEvaluationIso (X : C) :
    homSheafFunctor R N ⋙ SheafOfModules.forget _ ⋙
        PresheafOfModules.evaluation _ (op X) ⋙ forget _ ≅
      (SheafOfModules.overFunctor.{u,u,u,u} ((sheafCompose J (forget₂ CommRingCat RingCat)).obj R) X).op ⋙ yoneda.obj (N.over X) :=
…

Mentions: OAI.CoherentDual.homSheafFunctor

instance OAI.CoherentDual.homSheafEvaluation_preservesLimits line 400
instance OAI.CoherentDual.homSheafModuleEvaluation_preservesLimits line 412
instance OAI.CoherentDual.homSheafFunctor_preservesLimits line 423
Source documentation
Local linear Hom is left exact, because morphisms out of colimits turn into limits after restriction to every slice site.
```
instance homSheafFunctor_preservesLimits :
    PreservesLimitsOfSize.{u,u} (homSheafFunctor R N) where
…
```
Mentions: OAI.CoherentDual.homSheafFunctor
instance OAI.CoherentDual.homSheafFunctor_additive line 445
def OAI.CoherentDual.homCokernelIso line 464
Source documentation
Dualizing a genuine presentation gives the actual kernel. This is the kernel description used to prove coherence of the model dual, not a postulated exactness property of an abstract replacement dual.
```
def homCokernelIso (f : M ⟶ M') :
    homSheaf R (cokernel f) N ≅ kernel ((homSheafFunctor R N).map f.op) :=
…
```
Mentions: OAI.CoherentDual.homSheaf, OAI.CoherentDual.homSheafFunctor
def OAI.CoherentDual.homFreeIso line 487
Source documentation
The genuine internal Hom out of a free sheaf is the product of the target sheaf, with no presentation/exactness assumed.
```
def homFreeIso : homSheaf R (SheafOfModules.free I) N ≅ ∏ᶜ (fun (_ : I) => N) :=
…
```
Mentions: OAI.CoherentDual.homSheaf
def OAI.CoherentDual.dualFiniteFreeIso line 496
Source documentation
The dual of a finite free sheaf really is the same finite free sheaf.
```
def dualFiniteFreeIso :
    homSheaf R (SheafOfModules.free I) (SheafOfModules.unit _) ≅
      SheafOfModules.free I := by
…
```
Mentions: OAI.CoherentDual.homSheaf
def OAI.CoherentDual.kernelConjugateIso line 515
Source documentation
Transport a kernel through isomorphisms of its source and target.
```
def kernelConjugateIso (f : A ⟶ B) (eA : A ≅ A') (eB : B ≅ B') :
    kernel f ≅ kernel (eA.inv ≫ f ≫ eB.hom) :=
…
```
instance OAI.CoherentLocality.presentationMap_finite line 534
lemma OAI.CoherentLocality.finitePresentation_of_presentation line 551
instance OAI.CoherentLocality.bind_finite line 568
lemma OAI.CoherentLocality.finitePresentation_of_coversTop line 584
instance OAI.CoherentRestriction.preservesMonomorphisms line 597
instance OAI.CoherentRestriction.additive line 609
instance OAI.CoherentRestriction.preservesHomology line 614
instance OAI.CoherentRestriction.preservesFiniteLimits line 617
lemma OAI.CoherentExactAffine.localizations_comap_eq_map line 625
lemma OAI.CoherentExactAffine.comap_injective line 636
lemma OAI.CoherentExactAffine.tilde_map_app_injective line 647
instance OAI.CoherentExactAffine.preservesMonomorphisms line 652
instance OAI.CoherentExactAffine.preservesHomology line 660
instance OAI.CoherentExactAffine.preservesFiniteLimits line 663

lemma OAI.CoherentGlobal.exists_presentation_tilde line 672

Source documentation

A finite module on a Noetherian affine has a finite global presentation of its associated sheaf.

lemma exists_presentation_tilde {A : CommRingCat} [IsNoetherianRing A]
    (M : ModuleCat A) [Module.Finite A M] :
    ∃ P : (tilde M).Presentation, P.IsFinite := by
…

lemma OAI.CoherentGlobal.exists_presentation_kernel_tilde line 688
lemma OAI.CoherentGlobal.exists_presentation_kernel line 705
lemma OAI.CoherentGlobal.exists_presentation_kernel_free line 715
Source documentation
On a Noetherian affine, an actual kernel between finite free sheaves has a global finite presentation. This supplies the local input for duals.
```
lemma exists_presentation_kernel_free {A : CommRingCat} [IsNoetherianRing A]
    {I J : Type} [Finite I] [Finite J]
    (f : SheafOfModules.free (R := (Spec A).ringCatSheaf) I ⟶ SheafOfModules.free J) :
…
```
lemma OAI.CoherentGlobal.exists_presentation_iso line 740
lemma OAI.CoherentGlobal.exists_presentation_kernel_restrict line 756
lemma OAI.CoherentGlobal.exists_presentation_affine_over line 775

lemma OAI.CoherentGlobal.coherent_kernel_free line 812

Source documentation

An actual kernel of a map between finite free sheaves on a locally Noetherian scheme is a finite-presentation sheaf.

lemma coherent_kernel_free {X : Scheme} [IsLocallyNoetherian X]
    {I J : Type} [Finite I] [Finite J]
    (f : SheafOfModules.free (R := X.ringCatSheaf) I ⟶ SheafOfModules.free J) :
…

lemma OAI.CoherentLocality.finitePresentation_pushforward line 842
lemma OAI.CoherentLocality.finitePresentation_pushforward_of_isLeftAdjoint line 862
lemma OAI.CoherentDual.coherent_dual_of_global_presentation line 891
Source documentation
The actual structure-sheaf dual of a globally finitely presented sheaf on a locally Noetherian scheme is coherent.
```
lemma coherent_dual_of_global_presentation :
    (homSheaf X.sheaf M (SheafOfModules.unit _)).IsFinitePresentation := by
…
```
Mentions: OAI.CoherentDual.homSheaf
lemma OAI.CoherentGlobal.opensDense line 925
lemma OAI.CoherentGlobal.opensPreservesHypercovers line 929
lemma OAI.CoherentGlobal.opensOverPostContinuous line 936
lemma OAI.CoherentGlobal.finitePresentation_overEquiv_inverse line 946