CMPuncture.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

Reflexivity and punctured pullback of a finite module of depth three.

lemma OAI.ExplicitCone.module_reflexive_from_depth_three line 10
abbrev OAI.SourceConeMorphism.punctureInclusion line 22
instance OAI.SourceConeMorphism.punctureInclusion_comp_p_openImmersion line 24
def OAI.SourceConeMorphism.E_punctureIso line 28
def OAI.CoherentBaseChange.pushforwardRestrictSource line 47
def OAI.CoherentBaseChange.pushforwardRestrictTarget line 50
def OAI.CoherentBaseChange.pushforwardRestrictAppIso line 54
Source documentation
Finite-open restriction of pushforward, on sections.
```
def pushforwardRestrictAppIso (V : U.toScheme.Opens) :
    ((pushforwardRestrictSource f U M).val.obj (op V)) ≅
      ((pushforwardRestrictTarget f U M).val.obj (op V)) := by
…
```
Mentions: OAI.CoherentBaseChange.pushforwardRestrictSource, OAI.CoherentBaseChange.pushforwardRestrictTarget
lemma OAI.CoherentBaseChange.pushforwardRestrictAppIso_naturality line 69
def OAI.CoherentBaseChange.pushforwardRestrictIso line 89
Source documentation
Open base change for sheaves of modules; no assumption of flat base change or quasicoherence is needed for restriction to an open.
```
def pushforwardRestrictIso :
    (restrictFunctor U.ι).obj ((pushforward f).obj M) ≅
      (pushforward (f ∣_ U)).obj ((restrictFunctor (f ⁻¹ᵁ U).ι).obj M) :=
…
```
lemma OAI.CoherentGlobal.exists_finite_module_of_presentation line 106
Source documentation
A finite global presentation on an affine scheme is the associated sheaf of a finite module, via the finite cokernel of its presentation.
```
lemma exists_finite_module_of_presentation {R : CommRingCat}
    (M : (Spec R).Modules) (P : M.Presentation) [P.IsFinite] :
    ∃ N : ModuleCat R, Module.Finite R N ∧ Nonempty (tilde N ≅ M) := by
…
```
lemma OAI.CoherentGlobal.exists_presentation_kernel_of_presentations line 138
lemma OAI.CoherentGlobal.exists_presentation_cokernel_tilde line 150
lemma OAI.CoherentGlobal.exists_presentation_cokernel_of_presentations line 158
lemma OAI.CoherentGlobal.exists_presentation_affine_below line 180
Source documentation
Refine any one finite presentation chart to an arbitrary affine open inside it. This is used to put two coherent sheaves in finite module form on the same affine cover, without assuming global finite generation.
```
lemma exists_presentation_affine_below {X : Scheme} (M : X.Modules) (U : X.Opens)
    (P : (M.over U).Presentation) [P.IsFinite] (V : X.affineOpens) (hV : V.1 ≤ U) :
    ∃ Q : ((restrictFunctor (V.2.isoSpec.inv ≫ V.1.ι)).obj M).Presentation,
      Q.IsFinite := by
…
```
lemma OAI.CoherentGlobal.exists_presentation_prod_of_presentations line 200

lemma OAI.CoherentGlobal.exists_common_affine_refinement line 226

Source documentation

An affine common refinement of any two open covers.

lemma exists_common_affine_refinement {X : Scheme.{0}} {I J : Type}
    (A : I → X.Opens) (B : J → X.Opens)
    (hA : (⨆ i, A i) = ⊤) (hB : (⨆ j, B j) = ⊤) :
    ∃ (K : Type) (U : K → X.affineOpens), (⨆ k, (U k).1) = ⊤ ∧
      ∀ k, ∃ i j, (U k).1 ≤ A i ∧ (U k).1 ≤ B j := by
…

lemma OAI.CoherentGlobal.exists_common_affine_presentations line 246

Source documentation

Two coherent sheaves admit finite module presentations on the same affine open cover. No global generation assumption is imposed.

lemma exists_common_affine_presentations {X : Scheme.{0}} (M N : X.Modules)
    [M.IsFinitePresentation] [N.IsFinitePresentation] :
    ∃ (I : Type) (U : I → X.affineOpens),
      (⨆ i, (U i).1) = ⊤ ∧ ∀ i,
      (∃ P : ((restrictFunctor ((U i).2.isoSpec.inv ≫ (U i).1.ι)).obj M).Presentation,
        P.IsFinite) ∧
      (∃ P : ((restrictFunctor ((U i).2.isoSpec.inv ≫ (U i).1.ι)).obj N).Presentation,
        P.IsFinite) := by
…

lemma OAI.CoherentGlobal.coherent_kernel line 271
Source documentation
The coherent sheaves on a locally Noetherian scheme are closed under kernels. The proof works on a common affine cover and descends.
```
lemma coherent_kernel {X : Scheme} [IsLocallyNoetherian X]
    {M N : X.Modules} [M.IsFinitePresentation] [N.IsFinitePresentation] (f : M ⟶ N) :
    (kernel f).IsFinitePresentation := by
…
```
lemma OAI.CoherentGlobal.coherent_cokernel line 293
lemma OAI.CoherentGlobal.coherent_prod line 313
instance OAI.CoherentGlobal.coherentContainsZero line 335
instance OAI.CoherentGlobal.coherentClosedKernels line 340
instance OAI.CoherentGlobal.coherentClosedCokernels line 349
instance OAI.CoherentGlobal.coherentClosedBinaryProducts line 358
instance OAI.CoherentGlobal.coherentClosedFiniteProducts line 368
abbrev OAI.CoherentGlobal.Coh line 373
Source documentation
The abelian category of coherent structure-sheaf modules.
```
abbrev Coh (X : Scheme) :=
…
```
instance OAI.CoherentGlobal.(instance at line 376) line 376
lemma OAI.CoherentGlobal.coherent_restrict line 387
lemma OAI.CoherentGlobal.coherent_over_of_restrict line 412
lemma OAI.CoherentGlobal.coherent_of_affine_restrict line 423
def OAI.ModuleCat.restrictScalarsAlgebraEquiv line 441
def OAI.ModuleCat.extendScalarsTensorEquiv line 448
lemma OAI.CoherentGlobal.finiteGamma_of_presentation line 478
lemma OAI.CoherentGlobal.exists_presentation_restrict_below line 486
lemma OAI.CoherentGlobal.exists_presentation_basicOpen_below line 505

def OAI.CoherentGlobal.affinePullbackGammaIso line 538

Source documentation

Affine pullback on a quasicoherent sheaf, on global sections.

def affinePullbackGammaIso {R S : CommRingCat.{0}} (f : R ⟶ S)
    (M : (Spec R).Modules) [M.IsQuasicoherent] :
    moduleSpecΓFunctor.obj ((Scheme.Modules.pullback (Spec.map f)).obj M) ≅
      (ModuleCat.extendScalars f.hom).obj (moduleSpecΓFunctor.obj M) :=
…

lemma OAI.CoherentGlobal.finite_extendScalarsGamma_of_restrict_presentation line 547
lemma OAI.CoherentGlobal.finite_localizedModule_of_extendScalars line 559
lemma OAI.CoherentGlobal.finite_localizedGamma_of_basicOpen_presentation line 568

lemma OAI.CoherentGlobal.basicOpen_refinement_span line 579

Source documentation

A basis of principal opens subordinate to any open cover spans the unit ideal.

lemma basicOpen_refinement_span {R : CommRingCat.{0}} {I : Type}
    (U : I → (Spec R).Opens) (hU : (⨆ i, U i) = ⊤) :
    Ideal.span {g : R | ∃ i, PrimeSpectrum.basicOpen g ≤ U i} = ⊤ := by
…

lemma OAI.CoherentGlobal.finiteGamma_of_coherent line 595
Source documentation
Every coherent sheaf on an affine scheme has a finite module of sections. Finiteness is descended from its finite local presentations, not assumed from an abstract equivalence with finite modules.
```
lemma finiteGamma_of_coherent {R : CommRingCat.{0}} (M : (Spec R).Modules)
    [M.IsFinitePresentation] : Module.Finite R (moduleSpecΓFunctor.obj M) := by
…
```
lemma OAI.CoherentGlobal.finite_restrictScalars line 619

lemma OAI.CoherentGlobal.coherent_affinePushforward line 632

Source documentation

Finite pushforward of a coherent sheaf on an affine scheme is coherent, proved from its affine module of sections.

lemma coherent_affinePushforward {A B : CommRingCat.{0}} [IsNoetherianRing A]
    (f : A ⟶ B) (hf : f.hom.Finite) (M : (Spec B).Modules) [M.IsFinitePresentation] :
    ((Scheme.Modules.pushforward (Spec.map f)).obj M).IsFinitePresentation := by
…

def OAI.CoherentGlobal.pushforwardIsoRestrict line 659
Source documentation
Pushforward under a scheme isomorphism is restriction along its inverse.
```
def pushforwardIsoRestrict {X Y : Scheme.{0}} (e : X ≅ Y) :
    pushforward e.hom ≅ restrictFunctor e.inv := by
…
```
lemma OAI.CoherentGlobal.coherent_pushforward_iso line 670

lemma OAI.CoherentGlobal.coherent_pushforward_affine line 677

Source documentation

Affine charts, without assuming that the affine schemes are definitionally Spec.

lemma coherent_pushforward_affine {X Y : Scheme.{0}} [IsAffine X] [IsAffine Y]
    [IsLocallyNoetherian Y] (f : X ⟶ Y) [IsFinite f]
    (M : X.Modules) [M.IsFinitePresentation] :
    ((pushforward f).obj M).IsFinitePresentation := by
…

lemma OAI.CoherentGlobal.coherent_pushforward line 700

Source documentation

Finite pushforward preserves the coherent category.

lemma coherent_pushforward {X Y : Scheme.{0}} [IsLocallyNoetherian Y]
    (f : X ⟶ Y) [IsFinite f] (M : X.Modules) [M.IsFinitePresentation] :
    ((pushforward f).obj M).IsFinitePresentation := by
…

instance OAI.CoherentGlobal.affineGamma_additive line 723

def OAI.CoherentGlobal.shortComplexTildeIso line 728

Source documentation

The affine module/sheaf comparison respects short complexes.

def shortComplexTildeIso {R : CommRingCat.{0}} (S : ShortComplex (Spec R).Modules)
    [IsIso (fromTildeΓ S.X₁)] [IsIso (fromTildeΓ S.X₂)] [IsIso (fromTildeΓ S.X₃)] :
    (S.map (moduleSpecΓFunctor (R := R))).map (tilde.functor R) ≅ S :=
…

lemma OAI.CoherentGlobal.exact_iff_affineGamma line 738

lemma OAI.CoherentGlobal.exact_affinePushforward line 746

Source documentation

Affine pushforward is exact on the quasicoherent sheaves; there is no claim that arbitrary sheaf pushforward is exact.

lemma exact_affinePushforward {A B : CommRingCat.{0}} (f : A ⟶ B)
    (S : ShortComplex (Spec B).Modules)
    [S.X₁.IsQuasicoherent] [S.X₂.IsQuasicoherent] [S.X₃.IsQuasicoherent]
    (hS : S.Exact) : (S.map (pushforward (Spec.map f))).Exact := by
…

lemma OAI.CoherentGlobal.affine_below_cover line 776
Source documentation
Affine opens below a fixed open form an open cover of that open.
```
lemma affine_below_cover {X : Scheme.{0}} (U : X.Opens) :
    U ≤ ⨆ V : {V : X.affineOpens // V.1 ≤ U}, V.1.1 := by
…
```
lemma OAI.CoherentGlobal.hom_ext_affine line 782
lemma OAI.CoherentGlobal.isZero_of_affine_restrict line 808

lemma OAI.CoherentGlobal.exact_of_affine_restrict line 816

Source documentation

Exactness of module sheaves is local on affine opens.

lemma exact_of_affine_restrict {X : Scheme.{0}} (S : ShortComplex X.Modules)
    (h : ∀ U : X.affineOpens, (S.map (restrictFunctor U.1.ι)).Exact) : S.Exact := by
…