OAI/AlgebraicGeometry/SurfaceCones/TensorLineCoherent.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ActualSheafTensor.tensorLeft_additive line 9
2. lemma OAI.ActualSheafTensor.coherent_tensor_line line 18

   Source documentation

   A line bundle tensored with a coherent sheaf is coherent. The proof descends the tensor sheaf from its local unit trivializations.

   lemma coherent_tensor_line {X : Scheme.{0}} (L M : X.Modules)
       (d : LineTrivialization X.sheaf L) [M.IsFinitePresentation] :
       ((tensorLeft X.sheaf L).obj M).IsFinitePresentation := by
   …

   Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.tensorLeft

3. def OAI.ActualSheafTensor.coherentTensorLine line 38

   Source documentation

   The Cartier line twist on the abelian category of coherent sheaves.

   def coherentTensorLine {X : Scheme.{0}} (L : X.Modules)
       (d : LineTrivialization X.sheaf L) : CoherentGlobal.Coh X ⥤ CoherentGlobal.Coh X :=
   …

   Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.CoherentGlobal.Coh

4. instance OAI.ActualSheafTensor.coherentTensorLine_additive line 45
5. lemma OAI.ActualSheafTensor.coherentTensorLine_exact line 53
6. instance OAI.ActualSheafTensor.coherentTensorLine_preservesHomology line 71
7. def OAI.CoherentLocality.freePresentation line 92

   Source documentation

   The finite free sheaf has the presentation with no relations.

   def freePresentation (I : Type u) : (SheafOfModules.free (R := R) I).Presentation :=
   …

8. instance OAI.CoherentLocality.freePresentation_finite line 99
9. lemma OAI.CoherentLocality.finitePresentation_free line 109
10. lemma OAI.CoherentLocality.finitePresentation_unit line 113
11. lemma OAI.ActualSheafTensor.coherent_line line 127

    Source documentation

    Finite presentation of a line sheaf, descended from its unit trivializations rather than included in the line data.

    lemma coherent_line {X : Scheme.{0}} (L : X.Modules)
        (d : LineTrivialization X.sheaf L) : L.IsFinitePresentation := by
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization

12. def OAI.ActualSheafTensor.coherentIdealAction line 138

    Source documentation

    The resolution morphism for an Cartier line ideal, inside the category of coherent sheaves. The source is the tensor twist.

    def coherentIdealAction {X : Scheme.{0}} (L : X.Modules)
        (d : LineTrivialization X.sheaf L) (i : L ⟶ SheafOfModules.unit _) :
        coherentTensorLine L d ⟶ 𝟭 (CoherentGlobal.Coh X) where
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.coherentTensorLine, OAI.CoherentGlobal.Coh

13. def OAI.ActualSheafTensor.coherentCartierKernel line 148

    Source documentation

    The coherent first Tor object computed by the Cartier line resolution, viewed on the ambient scheme.

    def coherentCartierKernel {X : Scheme.{0}} [IsLocallyNoetherian X] (L : X.Modules)
        (d : LineTrivialization X.sheaf L) (i : L ⟶ SheafOfModules.unit _) :
        CoherentGlobal.Coh X ⥤ CoherentGlobal.Coh X :=
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.CoherentGlobal.Coh

14. def OAI.ActualSheafTensor.coherentCartierCokernel line 153
15. lemma OAI.ActualSheafTensor.tensorOverIso_inv_adjoint line 179
16. lemma OAI.ActualSheafTensor.idealAction_over_inv line 196

    Source documentation

    Restriction compatibility for the ideal multiplication. This identifies the global Cartier resolution with the local principal one.

    lemma idealAction_over_inv {L : SheafOfModules.{u} (ringSheaf R)}
        (i : L ⟶ SheafOfModules.unit _) (M : SheafOfModules.{u} (ringSheaf R)) :
        (tensorOverIso R U L M).inv ≫
            (SheafOfModules.overFunctor _ U).map ((idealAction R i).app M) =
          (idealAction (R.over U) ((SheafOfModules.overFunctor _ U).map i)).app (M.over U) := by
    …

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

17. lemma OAI.CartierCentrality.of_iso line 232

    Source documentation

    Every natural endomorphism of a functor naturally isomorphic to the identity commutes with that functor.

    lemma of_iso (T : C ⥤ C) (e : T ≅ 𝟭 C) (ε : T ⟶ 𝟭 C) (X : C) :
        ε.app (T.obj X) = T.map (ε.app X) := by
    …

18. lemma OAI.CartierCentrality.map_eq line 245

    Source documentation

    Centrality descends through the natural tensor-restriction isomorphism.

    lemma map_eq (T : C ⥤ C) (U : D ⥤ D) (F : C ⥤ D)
        (ρ : T ⋙ F ≅ F ⋙ U) (ε : T ⟶ 𝟭 C) (δ : U ⟶ 𝟭 D)
        (h : ∀ X, ρ.hom.app X ≫ δ.app (F.obj X) = F.map (ε.app X))
        (hδ : ∀ Y, δ.app (U.obj Y) = U.map (δ.app Y)) (X : C) :
        F.map (ε.app (T.obj X)) = F.map (T.map (ε.app X)) := by
    …

19. lemma OAI.ActualSheafTensor.idealAction_central line 280

    Source documentation

    Multiplication by a line ideal commutes with its tensor twist, as checked on a trivializing cover.

    lemma idealAction_central {L : SheafOfModules.{u} (ringSheaf R)}
        (d : LineTrivialization R L) (i : L ⟶ SheafOfModules.unit _)
        (M : SheafOfModules.{u} (ringSheaf R)) :
        (idealAction R i).app ((tensorLeft R L).obj M) =
          (tensorLeft R L).map ((idealAction R i).app M) := by
    …

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

20. lemma OAI.CartierAnnihilator.kernel_annihilated line 324

    Source documentation

    The kernel of a central Cartier action is annihilated by that same action. Naturality alone would not suffice without centrality.

    lemma kernel_annihilated (M : C) : ε.app (kernel (ε.app M)) = 0 := by
    …

21. lemma OAI.CartierAnnihilator.cokernel_annihilated line 334

    Source documentation

    Right exactness and centrality make the cokernel a module on the Cartier zero locus.

    lemma cokernel_annihilated [T.PreservesEpimorphisms] (M : C) :
        ε.app (cokernel (ε.app M)) = 0 := by
    …

22. lemma OAI.ActualSheafTensor.coherentIdealAction_central line 348

    Source documentation

    Centrality for the coherent Cartier resolution.

    lemma coherentIdealAction_central {X : Scheme.{0}} (L : X.Modules)
        (d : LineTrivialization X.sheaf L) (i : L ⟶ SheafOfModules.unit _)
        (M : CoherentGlobal.Coh X) :
        (coherentIdealAction L d i).app ((coherentTensorLine L d).obj M) =
          (coherentTensorLine L d).map ((coherentIdealAction L d i).app M) := by
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.CoherentGlobal.Coh, OAI.ActualSheafTensor.coherentIdealAction, OAI.ActualSheafTensor.coherentTensorLine

23. lemma OAI.ActualSheafTensor.coherentCartierKernel_annihilated line 358

    Source documentation

    The first Cartier Tor object is annihilated by the ideal as a coherent sheaf on the ambient scheme.

    lemma coherentCartierKernel_annihilated {X : Scheme.{0}} [IsLocallyNoetherian X]
        (L : X.Modules) (d : LineTrivialization X.sheaf L)
        (i : L ⟶ SheafOfModules.unit _) (M : CoherentGlobal.Coh X) :
        (coherentIdealAction L d i).app
          (kernel ((coherentIdealAction L d i).app M)) = 0 :=
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.CoherentGlobal.Coh, OAI.ActualSheafTensor.coherentIdealAction

24. lemma OAI.ActualSheafTensor.coherentCartierCokernel_annihilated line 367

    Source documentation

    The coherent restriction object is killed by the ideal.

    lemma coherentCartierCokernel_annihilated {X : Scheme.{0}} [IsLocallyNoetherian X]
        (L : X.Modules) (d : LineTrivialization X.sheaf L)
        (i : L ⟶ SheafOfModules.unit _) (M : CoherentGlobal.Coh X) :
        (coherentIdealAction L d i).app
          (cokernel ((coherentIdealAction L d i).app M)) = 0 := by
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.CoherentGlobal.Coh, OAI.ActualSheafTensor.coherentIdealAction

25. lemma OAI.ActualSheafTensor.idealAction_annihilates_sections line 395

    Source documentation

    Vanishing of the ideal action implies annihilation of every section.

    lemma idealAction_annihilates_sections {X : Scheme.{0}} {L : X.Modules}
        (i : L ⟶ SheafOfModules.unit _) (M : X.Modules)
        (h : (idealAction X.sheaf i).app M = 0)
        (U : X.Opens) (l : L.val.obj (op U)) (m : M.val.obj (op U)) :
        (i.val.app (op U) l) • m = 0 := by
    …

    Mentions: OAI.ActualSheafTensor.idealAction

26. lemma OAI.ActualSheafTensor.affine_idealAction_torsion line 404
27. lemma OAI.ActualSheafTensor.coherentCartierKernel_principal_descent line 417

    Source documentation

    The coherent Cartier kernel descends to the affine principal divisor. The section hypothesis just identifies the local Cartier equation with a section of the given ideal line.

    lemma coherentCartierKernel_principal_descent {R : CommRingCat.{0}}
        [IsNoetherianRing R] (L : (Spec R).Modules)
        (d : LineTrivialization (Spec R).sheaf L) (i : L ⟶ SheafOfModules.unit _)
        (M : CoherentGlobal.Coh (Spec R)) (t : R) (l : L.val.obj (op ⊤))
        (hl : i.val.app (op ⊤) l = (Scheme.ΓSpecIso R).inv.hom t) :
        ∃ N : (Spec (CommRingCat.of (R ⧸ Ideal.span ({t} : Set R)))).Modules,
          N.IsFinitePresentation ∧ Nonempty
            ((Scheme.Modules.pushforward (Spec.map (CommRingCat.ofHom
              (Ideal.Quotient.mk (Ideal.span ({t} : Set R)))))).obj N ≅
              (kernel ((coherentIdealAction L d i).app M)).obj) := by
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.CoherentGlobal.Coh, OAI.ActualSheafTensor.coherentIdealAction

28. lemma OAI.ActualSheafTensor.coherentCartierCokernel_principal_descent line 434

    Source documentation

    The coherent cokernel (ordinary restriction) descends as well.

    lemma coherentCartierCokernel_principal_descent {R : CommRingCat.{0}}
        [IsNoetherianRing R] (L : (Spec R).Modules)
        (d : LineTrivialization (Spec R).sheaf L) (i : L ⟶ SheafOfModules.unit _)
        (M : CoherentGlobal.Coh (Spec R)) (t : R) (l : L.val.obj (op ⊤))
        (hl : i.val.app (op ⊤) l = (Scheme.ΓSpecIso R).inv.hom t) :
        ∃ N : (Spec (CommRingCat.of (R ⧸ Ideal.span ({t} : Set R)))).Modules,
          N.IsFinitePresentation ∧ Nonempty
            ((Scheme.Modules.pushforward (Spec.map (CommRingCat.ofHom
              (Ideal.Quotient.mk (Ideal.span ({t} : Set R)))))).obj N ≅
              (cokernel ((coherentIdealAction L d i).app M)).obj) := by
    …

    Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.CoherentGlobal.Coh, OAI.ActualSheafTensor.coherentIdealAction

29. lemma OAI.CoherentGlobal.affine_chart_torsion line 458
30. lemma OAI.CoherentGlobal.annihilated_restrict line 479
31. lemma OAI.CoherentGlobal.exists_closed_preimage_of_annihilated line 501
32. def OAI.ActualCartier.structureMap line 528

    Source documentation

    The map from the ambient structure sheaf to the pushed-forward structure sheaf; its section maps are precisely the scheme comorphism.

    def structureMap : SheafOfModules.unit Y.ringCatSheaf ⟶
        (pushforward f).obj (SheafOfModules.unit X.ringCatSheaf) :=
    …

33. def OAI.ActualCartier.idealSheaf line 532

    Source documentation

    The ideal sheaf of a closed immersion, defined as a sheaf kernel.

    def idealSheaf : Y.Modules := kernel (structureMap f)

    Mentions: OAI.ActualCartier.structureMap

34. def OAI.ActualCartier.idealι line 533
35. lemma OAI.ActualCartier.ideal_section_lift line 535
36. lemma OAI.ActualCartier.exists_coherent_preimage line 551

    Source documentation

    Killing the ideal action is sufficient for descent to the actual closed subscheme. No support or divisor-category object is postulated.

    lemma exists_coherent_preimage {X Y : Scheme.{0}} [IsLocallyNoetherian Y]
        (f : X ⟶ Y) [IsClosedImmersion f] (M : Y.Modules) [M.IsFinitePresentation]
        (h : (ActualSheafTensor.idealAction Y.sheaf (idealι f)).app M = 0) :
        ∃ N : CoherentGlobal.Coh X, Nonempty ((pushforward f).obj N.obj ≅ M) := by
    …

    Mentions: OAI.ActualSheafTensor.idealAction, OAI.ActualCartier.idealι, OAI.CoherentGlobal.Coh

37. def OAI.ActualSheafTensor.pure line 577

    Source documentation

    The canonical pure-tensor section of the tensor sheaf.

    def pure (M N : SheafOfModules.{u} (ringSheaf R)) (U : Cᵒᵖ)
        (x : M.val.obj U) (y : N.val.obj U) : (tensor R M N).val.obj U :=
    …

    Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensor

38. lemma OAI.ActualSheafTensor.tensor_hom_ext line 583
39. lemma OAI.ActualSheafTensor.tensorLeftMap_pure line 597
40. lemma OAI.ActualSheafTensor.leftUnitIso_pure line 609
41. def OAI.TensorChangeScalars.transportEquiv line 636

    Source documentation

    The identity on underlying sections, with the scalar action transported along a coefficient-ring isomorphism.

    def transportEquiv : M ≃ₛₗ[e.toRingHom]
        ((ModuleCat.restrictScalars e.symm.toRingHom).obj M) where
    …

42. def OAI.TensorChangeScalars.tensorEquiv line 649

    Source documentation

    Restriction through a ring isomorphism commutes with tensor product. The formula on pure tensors is literally the identity on both factors.

    def tensorEquiv :
        ((ModuleCat.restrictScalars e.symm.toRingHom).obj (ModuleCat.of R (M ⊗[R] N))) ≃ₗ[S]
          (((ModuleCat.restrictScalars e.symm.toRingHom).obj M) ⊗[S]
            ((ModuleCat.restrictScalars e.symm.toRingHom).obj N)) where
    …

43. lemma OAI.TensorChangeScalars.tensorEquiv_tmul line 670
44. lemma OAI.TensorChangeScalars.tensorEquiv_symm_tmul line 673
45. def OAI.ModuleSheafification.comparison line 696

    Source documentation

    The canonical sheafification comparison for modules and any continuous cocontinuous site functor, including nontrivial scalar transport.

    def comparison (P : PresheafOfModules.{u} R.obj) :
        (PresheafOfModules.sheafification (𝟙 S.obj)).obj
            ((PresheafOfModules.pushforward φ.hom).obj P) ⟶
          (SheafOfModules.pushforward φ).obj
            ((PresheafOfModules.sheafification (𝟙 R.obj)).obj P) :=
    …

46. lemma OAI.ModuleSheafification.comparison_toSheaf line 705
47. instance OAI.ModuleSheafification.comparison_isIso line 715
48. lemma OAI.ModuleSheafification.comparison_unit line 724

    Source documentation

    The defining unit identity of the comparison, retained so that projection formulas can be checked on sections without unfolding sheafification.

    lemma comparison_unit (P : PresheafOfModules.{u} R.obj) :
        (PresheafOfModules.sheafificationAdjunction (𝟙 S.obj)).unit.app
            ((PresheafOfModules.pushforward φ.hom).obj P) ≫
          (SheafOfModules.forget S).map (comparison F φ P) =
        (PresheafOfModules.pushforward φ.hom).map
          ((PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).unit.app P) := by
    …

    Mentions: OAI.ModuleSheafification.comparison

49. def OAI.ActualSheafTensor.schemeRingRestrictHom line 746

    Source documentation

    The coefficient-ring map for open-scheme restriction.

    def schemeRingRestrictHom : U.toScheme.ringCatSheaf ⟶
        (U.ι.opensFunctor.sheafPushforwardContinuous RingCat
          (Opens.grothendieckTopology U.toScheme) (Opens.grothendieckTopology X)).obj
          X.ringCatSheaf :=
    …

50. def OAI.ActualSheafTensor.schemePresheafRestrict line 756

    Source documentation

    The concrete presheaf restriction underlying open-scheme restriction.

    def schemePresheafRestrict : PresheafOfModules.{0} X.ringCatSheaf.obj ⥤
        PresheafOfModules.{0} U.toScheme.ringCatSheaf.obj :=
    …

51. def OAI.ActualSheafTensor.schemeSheafifyRestrictMap line 761

    Source documentation

    Canonical open restriction comparison for module sheafification.

    def schemeSheafifyRestrictMap (P : PresheafOfModules.{0} X.ringCatSheaf.obj) :
        (PresheafOfModules.sheafification (𝟙 U.toScheme.ringCatSheaf.obj)).obj
            ((schemePresheafRestrict X U).obj P) ⟶
          (restrictFunctor U.ι).obj
            ((PresheafOfModules.sheafification (𝟙 X.ringCatSheaf.obj)).obj P) :=
    …

    Mentions: OAI.ActualSheafTensor.schemePresheafRestrict

52. instance OAI.ActualSheafTensor.schemeSheafifyRestrictMap_isIso line 768
53. def OAI.ActualSheafTensor.schemePresheafTensorRestrictIso line 773

    Source documentation

    Tensor presheaves commute with restriction to an open subscheme.

    def schemePresheafTensorRestrictIso (M N : PresheafOfModules.{0} X.ringCatSheaf.obj) :
        (schemePresheafRestrict X U).obj
          (PresheafOfModulesOfCommRing.Monoidal.tensorObj (R := X.sheaf.obj) M N) ≅
    …

    Mentions: OAI.ActualSheafTensor.schemePresheafRestrict

54. def OAI.ActualSheafTensor.tensorSchemeRestrictIso line 791

    Source documentation

    The tensor sheaf commutes with open-scheme restriction.

    def tensorSchemeRestrictIso (M N : X.Modules) :
        (restrictFunctor U.ι).obj (tensor X.sheaf M N) ≅
          tensor U.toScheme.sheaf ((restrictFunctor U.ι).obj M) ((restrictFunctor U.ι).obj N) :=
    …

    Mentions: OAI.ActualSheafTensor.tensor

55. def OAI.ActualSheafTensor.LineTrivialization.schemeIso line 812

    Source documentation

    A slice-site line trivialization is an trivialization on the corresponding open subscheme; no extra local freeness hypothesis is added.

    def LineTrivialization.schemeIso (i : d.I) :
        (restrictFunctor (Scheme.Opens.ι (d.obj i))).obj L ≅ SheafOfModules.unit (Scheme.Opens.toScheme (d.obj i)).ringCatSheaf :=
    …