OAI/AlgebraicGeometry/SurfaceCones/CartierFactorization.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ActualCartier.global_power_sandwich_factorization line 36

   Source documentation

   The two cleared maps are inverse up to the indicated ideal power. Torsion freeness extends the equality from the puncture to the whole scheme.

   lemma global_power_sandwich_factorization
       (n : ℕ) {M N : Y.Modules} [N.IsFinitePresentation]
       (hN : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (N.val.obj U))
       (e : M.over (ActualOpenSupport.complement g) ≅
         N.over (ActualOpenSupport.complement g))
       (f : (power (tensorLeft Y.sheaf (idealSheaf g)) n).obj M ⟶ N)
       (a : (power (tensorLeft Y.sheaf (idealSheaf g)) n).obj N ⟶ M)
       (hf : f.over (ActualOpenSupport.complement g) =
         ((powerAction (tensorLeft Y.sheaf (idealSheaf g))
           (idealAction Y.sheaf (idealι g)) n).app M).over
             (ActualOpenSupport.complement g) ≫ e.hom)
       (ha : a.over (ActualOpenSupport.complement g) =
   …

   Mentions: OAI.ActualOpenSupport.complement, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι

2. lemma OAI.ActualCartier.idealMultiple_isZero_of_raw_factorization line 94

   Source documentation

   An ideal-power factorization annihilates the coherent quotient by the same exponent.

   lemma idealMultiple_isZero_of_raw_factorization
       {S : ShortComplex (Coh Y)} (hS : S.ShortExact) (n : ℕ)
       (a : (power (tensorLeft Y.sheaf (idealSheaf g)) n).obj S.X₂.obj ⟶ S.X₁.obj)
       (ha : a ≫ S.f.hom =
         (powerAction (tensorLeft Y.sheaf (idealSheaf g))
           (idealAction Y.sheaf (idealι g)) n).app S.X₂.obj) :
       IsZero (idealMultiple g d n S.X₃) := by
   …

   Mentions: OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι, OAI.ActualCartier.idealMultiple

3. lemma OAI.ActualCartier.exists_cleared_lattice_twice_bound line 119

   Source documentation

   The coherent lattice construction with the twice-clearing exponent, conormal-layer epimorphisms and divisor Grothendieck identity.

   lemma exists_cleared_lattice_twice_bound
       (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
       (hM : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (M.val.obj U))
       (hN : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (N.val.obj U))
       (e : M.over (ActualOpenSupport.complement g) ≅
         N.over (ActualOpenSupport.complement g)) :
       let L : Coh Y := ⟨N, inferInstance⟩
   …

   Mentions: OAI.ActualOpenSupport.complement

4. def OAI.ActualCartier.coherentFree line 171

   Source documentation

   The finite free coherent module sheaf.

   def coherentFree (Y : Scheme.{0}) (I : Type) [Finite I] : Coh Y :=
   …

5. lemma OAI.ActualCartier.free_sections_torsionFree line 177

   Source documentation

   On an integral scheme, the finite free sheaf is sectionwise torsion free, including empty opens.

   lemma free_sections_torsionFree (Y : Scheme.{0}) [IsIntegral Y]
       (I : Type) [Finite I] (U : Y.Opensᵒᵖ) :
       Module.IsTorsionFree (Y.sheaf.obj.obj U)
         ((SheafOfModules.free (R := Y.ringCatSheaf) I).val.obj U) := by
   …

6. def OAI.ActualCartier.restriction_freeIso line 192

   Source documentation

   The coherent restriction used by the Cartier resolution sends the finite free sheaf to the same finite free sheaf on the divisor.

   def restriction_freeIso (I : Type) [Finite I] :
       (restriction g d).obj (coherentFree Y I) ≅ coherentFree X I :=
   …

   Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.coherentFree

7. def OAI.ActualCartier.freeTwistedLayerQuotient line 205

   Source documentation

   The quotient map from the jth conormal twist of O_D^N to the jth quotient layer.

   def freeTwistedLayerQuotient {Q : Coh Y} {I : Type} [Finite I]
       (q : coherentFree Y I ⟶ Q) (j : ℕ) :
       (power (conormalFunctor g d) j).obj (coherentFree X I) ⟶ layer g d j Q :=
   …

   Mentions: OAI.ActualCartier.coherentFree, OAI.ActualCartier.conormalFunctor, OAI.ActualCartier.layer

8. instance OAI.ActualCartier.freeTwistedLayerQuotient_epi line 211
9. lemma OAI.ActualCartier.exists_free_cleared_lattice line 221

   Source documentation

   The sheaf-theoretic content of the divisor lattice construction for the finite free ambient lattice: a fixed puncture trivialization constructs the embedding, the finite twice-bound filtration, the divisor K₀ identity, and all the required quotients of conormal-twisted free sheaves.

   lemma exists_free_cleared_lattice [CompactSpace Y] [IsIntegral Y]
       (M : Y.Modules) [M.IsFinitePresentation]
       (hM : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (M.val.obj U))
       (N : ℕ)
       (e : M.over (ActualOpenSupport.complement g) ≅
         (SheafOfModules.free (R := Y.ringCatSheaf) (Fin N)).over
   …

   Mentions: OAI.ActualOpenSupport.complement

10. lemma OAI.SourceZeroSections.seriesOrigin_kernel line 264
11. lemma OAI.SourceZeroSections.seriesOrigin_range_compl line 273
12. lemma OAI.SourceZeroSections.completedPlaneZero_range line 285
13. lemma OAI.SourceZeroSections.planeComplement_eq line 302
14. def OAI.SourceConeMorphism.modelPushforwardComplementFreeIso line 313
15. def OAI.SourceConeMorphism.modelPushforwardOverFreeIso line 320

    Source documentation

    The slice-site framing for the generic lattice construction.

    def modelPushforwardOverFreeIso :
        (modelPushforward M).over (ActualOpenSupport.complement completedPlaneZero) ≅
          (SheafOfModules.free (R := V.ringCatSheaf) (basisIndex M hdepth)).over
    …

    Mentions: OAI.ActualOpenSupport.complement, OAI.SourceConeMorphism.basisIndex

16. def OAI.SourceZeroSections.planeIdealChartIso line 343
17. def OAI.SourceZeroSections.planeIdealLine line 353
18. lemma OAI.SourceZeroSections.planeIdeal_coherent line 357
19. instance OAI.SourceConeMorphism.sourcePlane_noetherian line 377
20. instance OAI.SourceConeMorphism.sourceV_compact line 384
21. instance OAI.SourceConeMorphism.basisIndex_fintype line 394
22. abbrev OAI.SourceConeMorphism.sourceFreeRank line 395
23. lemma OAI.SourceConeMorphism.sourceFreeRank_pos line 397
24. def OAI.SourceConeMorphism.modelPushforwardOverFinIso line 404
25. theorem OAI.SourceConeMorphism.exists_source_free_lattice line 415

    Source documentation

    Coherent lattice, finite conormal layers, K₀ identity, and quotients of conormal-twisted free sheaves for the finite pushforward. Every premise of the reused lattice theorem is supplied by the source.

    theorem exists_source_free_lattice :
        ∃ k : ℕ, ∀ n : ℕ, k ≤ n →
          ∃ a : clearedLattice completedPlaneZero planeIdealLine n (modelPushforward M) ⟶
              coherentFree V (Fin (sourceFreeRank M hdepth)),
            Mono a ∧
            ((cohInclusion V).map a).over (ActualOpenSupport.complement completedPlaneZero) =
              ((powerAction (tensorLeft V.sheaf (idealSheaf completedPlaneZero))
                (idealAction V.sheaf (idealι completedPlaneZero)) n).app (modelPushforward M)).over
                  (ActualOpenSupport.complement completedPlaneZero) ≫
                    (modelPushforwardOverFinIso M hdepth).hom ∧
            IsZero (idealMultiple completedPlaneZero planeIdealLine (n + n) (cokernel a)) ∧
            cls ((restriction completedPlaneZero planeIdealLine).obj
    …

    Mentions: OAI.SourceConeMorphism.sourceFreeRank, OAI.ActualOpenSupport.complement, OAI.SourceConeMorphism.modelPushforwardOverFinIso

26. instance OAI.SourceConeMorphism.sourceSurface_noetherian line 445
27. abbrev OAI.SourceConeMorphism.sourceRestriction line 448
28. abbrev OAI.SourceConeMorphism.coherentModel line 449
29. def OAI.SourceConeMorphism.sourceRestrictionIso line 452
30. lemma OAI.SourceConeMorphism.modelRestriction_torsionFree line 456
31. abbrev OAI.SourceConeMorphism.elementaryTransform line 464
32. lemma OAI.SourceConeMorphism.elementaryTransform_torsionFree line 468
33. lemma OAI.SourceConeMorphism.elementaryTransform_restriction_torsionFree line 478

    Source documentation

    The divisor restriction of an elementary transform is torsion-free when the chosen quotient is torsion-free.

    lemma elementaryTransform_restriction_torsionFree
        {B : Coh W} {G : Coh ExplicitCone.projectiveSurface}
        (q : sourceRestriction.obj B ⟶ G) [Epi q]
        (hB : ∀ U, Module.IsTorsionFree (W.sheaf.obj.obj U) (B.obj.val.obj U))
        (hP : ∀ U, Module.IsTorsionFree (ExplicitCone.projectiveSurface.sheaf.obj.obj U)
          ((sourceRestriction.obj B).obj.val.obj U))
        (hG : ∀ U, Module.IsTorsionFree (ExplicitCone.projectiveSurface.sheaf.obj.obj U)
          (G.obj.val.obj U))
        (U : ExplicitCone.projectiveSurface.Opensᵒᵖ) :
        Module.IsTorsionFree (ExplicitCone.projectiveSurface.sheaf.obj.obj U)
          ((sourceRestriction.obj (elementaryTransform q)).obj.val.obj U) := by
    …

    Mentions: OAI.ExplicitCone.projectiveSurface, OAI.SourceConeMorphism.elementaryTransform

34. lemma OAI.SourceConeMorphism.elementaryTransform_puncture line 500
35. abbrev OAI.SourceConeMorphism.sourceFramedOpen line 517
36. lemma OAI.SourceConeMorphism.sourceZero_preimage_framed line 518
37. structure OAI.SourceConeMorphism.ExtensionState line 523
38. def OAI.SourceConeMorphism.ExtensionState.initial line 534
39. def OAI.SourceConeMorphism.ExtensionState.transform line 542

    Source documentation

    The elementary transform constructs another admissible extension and preserves its punctured framing.

    def transform (B : ExtensionState M) {G : Coh ExplicitCone.projectiveSurface}
        (q : sourceRestriction.obj B.sheaf ⟶ G) [Epi q]
        (hG : ∀ U, Module.IsTorsionFree (ExplicitCone.projectiveSurface.sheaf.obj.obj U)
          (G.obj.val.obj U)) : ExtensionState M where
    …

    Mentions: OAI.SourceConeMorphism.ExtensionState, OAI.ExplicitCone.projectiveSurface

40. def OAI.SourceConeMorphism.ExtensionState.pushforward line 556
41. lemma OAI.SourceConeMorphism.ExtensionState.pushforward_torsionFree line 558
42. def OAI.SourceConeMorphism.ExtensionState.pushforwardFraming line 565
43. def OAI.SourceConeMorphism.ExtensionState.pushforwardOverFinIso line 574
44. theorem OAI.SourceConeMorphism.ExtensionState.exists_free_lattice line 606

    Source documentation

    The exact coherent K₀ statement and conormal-twisted quotient layers needed by the lattice inequality, for any constructed extension.

    theorem exists_free_lattice (B : ExtensionState M) :
        ∃ k : ℕ, ∀ n : ℕ, k ≤ n →
          ∃ a : clearedLattice completedPlaneZero planeIdealLine n B.pushforward.obj ⟶
              coherentFree V (Fin (sourceFreeRank M hdepth)),
            Mono a ∧
            ((cohInclusion V).map a).over (ActualOpenSupport.complement completedPlaneZero) =
              ((powerAction (tensorLeft V.sheaf (idealSheaf completedPlaneZero))
                (idealAction V.sheaf (idealι completedPlaneZero)) n).app B.pushforward.obj).over
                  (ActualOpenSupport.complement completedPlaneZero) ≫
                    (B.pushforwardOverFinIso hdepth).hom ∧
            IsZero (idealMultiple completedPlaneZero planeIdealLine (n + n) (cokernel a)) ∧
            cls ((restriction completedPlaneZero planeIdealLine).obj
    …

    Mentions: OAI.SourceConeMorphism.ExtensionState, OAI.SourceConeMorphism.sourceFreeRank, OAI.ActualOpenSupport.complement

45. def OAI.SourceConeMorphism.ExtensionState.restrictionPushforwardIso line 639
46. lemma OAI.SourceConeMorphism.ExtensionState.restrictionPushforward_class line 648
47. lemma OAI.ActualMateUnit.chosen_units line 667
48. lemma OAI.ActualMateUnit.three_iso_chain line 682
49. lemma OAI.ActualCartier.structure_comp line 703
50. lemma OAI.ActualCartier.structure_congr line 712
51. lemma OAI.ActualCartier.structure_square line 723
52. lemma OAI.ActualCartier.pullbackUnit_adj line 738
53. lemma OAI.ActualCartier.baseChange_structure line 747
54. lemma OAI.ActualCartier.restrictionPullbackIso_unit line 773
55. lemma OAI.ActualCartier.coherent_adjUnit_epi line 784
56. lemma OAI.ActualCartier.structureMap_epi line 797
57. lemma OAI.ActualRightExactIdeal.kernelComparison_epi line 820
58. def OAI.ActualRightExactIdeal.comparison line 829
59. instance OAI.ActualRightExactIdeal.comparison_epi line 834
60. lemma OAI.ActualRightExactIdeal.comparison_ι line 842