OAI/AlgebraicGeometry/SurfaceCones/CartierGluing.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Global denominator clearing for coherent lattices

This development accompanies A Complete Local Domain without a Small Cohen–Macaulay Module (OpenAI, 2026).

  1. def OAI.ActualCartier.restrictOverHom line 29

    Source documentation

    Restrict a slice-site module morphism to a smaller open.

    def restrictOverHom {M N : Y.Modules} {U V : Y.Opens} (h : V ≤ U)
    (a : M.over U ⟶ N.over U) : M.over V ⟶ N.over V :=
…
  2. lemma OAI.ActualCartier.exists_gluing_of_puncture line 38

    Source documentation

    Denominator-cleared local extensions of a fixed Cartier-puncture morphism agree on overlaps and glue.

    lemma exists_gluing_of_puncture {ι : Type*} (U : ι → Y.Opens)
    (hU : (⨆ i, U i) = ⊤)
    (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ⟶
      N.over (ActualOpenSupport.complement g))
    (a : ∀ i, M.over (U i) ⟶ N.over (U i))
    (ha : ∀ i (V : Y.Opens) (hi : V ≤ U i)
      (hV : V ≤ ActualOpenSupport.complement g) (x : M.val.obj (op V)),
      (a i).val.app (op (Over.mk (homOfLE hi))) x =
        e.val.app (op (Over.mk (homOfLE hV))) x) :
    ∃ f : M ⟶ N, ∀ i, f.over (U i) = a i := by
…

    Mentions: OAI.ActualOpenSupport.complement

  3. lemma OAI.ActualCartier.exists_mono_gluing_of_puncture line 68

    Source documentation

    Injective local extensions glue to an injective global extension.

    lemma exists_mono_gluing_of_puncture {ι : Type*} (U : ι → Y.Opens)
    (hU : (⨆ i, U i) = ⊤)
    (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ⟶
      N.over (ActualOpenSupport.complement g))
    (a : ∀ i, M.over (U i) ⟶ N.over (U i)) [∀ i, Mono (a i)]
    (ha : ∀ i (V : Y.Opens) (hi : V ≤ U i)
      (hV : V ≤ ActualOpenSupport.complement g) (x : M.val.obj (op V)),
      (a i).val.app (op (Over.mk (homOfLE hi))) x =
        e.val.app (op (Over.mk (homOfLE hV))) x) :
    ∃ f : M ⟶ N, Mono f ∧ ∀ i, f.over (U i) = a i := by
…

    Mentions: OAI.ActualOpenSupport.complement

  4. lemma OAI.ActualCartier.exists_mono_extension_of_local line 104

    Source documentation

    Compatible injective local extensions of a puncture morphism glue to an injective global extension of that morphism.

    lemma exists_mono_extension_of_local {ι : Type*} (U : ι → Y.Opens)
    (hU : (⨆ i, U i) = ⊤)
    (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ⟶
      N.over (ActualOpenSupport.complement g))
    (a : ∀ i, M.over (U i) ⟶ N.over (U i)) [∀ i, Mono (a i)]
    (ha : ∀ i (V : Y.Opens) (hi : V ≤ U i)
      (hV : V ≤ ActualOpenSupport.complement g) (x : M.val.obj (op V)),
      (a i).val.app (op (Over.mk (homOfLE hi))) x =
        e.val.app (op (Over.mk (homOfLE hV))) x) :
    ∃ f : M ⟶ N, Mono f ∧ f.over (ActualOpenSupport.complement g) = e := by
…

    Mentions: OAI.ActualOpenSupport.complement

  5. lemma OAI.ActualCartier.exists_uniform_mono_extension line 127

    Source documentation

    A finite cover admits a single bound for all local extension exponents. Every exponent beyond that bound gives a global injective extension preserving its specified puncture map.

    lemma exists_uniform_mono_extension {ι : Type*} [Fintype ι] (U : ι → Y.Opens)
    (hU : (⨆ i, U i) = ⊤) (M : ℕ → Y.Modules) (N : Y.Modules)
    [∀ n, (M n).IsFinitePresentation] [N.IsFinitePresentation]
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : ∀ n, (M n).over (ActualOpenSupport.complement g) ⟶
      N.over (ActualOpenSupport.complement g))
    (hloc : ∀ i, ∃ k : ℕ, ∀ n : ℕ, k ≤ n →
      ∃ a : (M n).over (U i) ⟶ N.over (U i), Mono a ∧
        ∀ (V : Y.Opens) (hi : V ≤ U i)
          (hV : V ≤ ActualOpenSupport.complement g) (x : (M n).val.obj (op V)),
          a.val.app (op (Over.mk (homOfLE hi))) x =
            (e n).val.app (op (Over.mk (homOfLE hV))) x) :
…

    Mentions: OAI.ActualOpenSupport.complement

  6. lemma OAI.ActualSheafTensor.idealAction_isIso_of_isIso line 161
  7. lemma OAI.CartierImageFiltration.powerAction_isIso line 170
  8. lemma OAI.kernel_ι_isIso_of_zero line 180
  9. lemma OAI.ActualCartier.ideal_puncture_isIso line 190

    Source documentation

    The kernel ideal of a closed part becomes the unit ideal on its open complement. This uses the pushforward sections.

    lemma ideal_puncture_isIso (U : Y.Opens) (hU : f ⁻¹ᵁ U = ⊥) :
    IsIso ((restrictFunctor U.ι).map (idealι f)) := by
…

    Mentions: OAI.ActualCartier.idealι

  10. lemma OAI.ActualCartier.ideal_power_puncture_isIso line 207

    Source documentation

    Every Cartier tensor power is invertible on the geometric puncture. In particular, a cleared lattice map retaining the original puncture identification really is an isomorphism there.

    lemma ideal_power_puncture_isIso (U : Y.Opens) (hU : f ⁻¹ᵁ U = ⊥)
    (n : ℕ) (M : Y.Modules) :
    IsIso ((restrictFunctor U.ι).map
      ((powerAction (tensorLeft Y.sheaf (idealSheaf f))
        (idealAction Y.sheaf (idealι f)) n).app M)) := by
…

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

  11. lemma OAI.ActualCartier.over_isIso_iff_restrict line 240

    Source documentation

    Isomorphy on a open subscheme and on its slice site are equivalent, using the restriction comparison equivalence.

    lemma over_isIso_iff_restrict (U : Y.Opens) {M N : Y.Modules} (a : M ⟶ N) :
    IsIso (a.over U) ↔ IsIso ((restrictFunctor U.ι).map a) :=
…
  12. lemma OAI.ActualCartier.preimage_complement line 246

    Source documentation

    The geometric complement has empty inverse image.

    lemma preimage_complement (g : X ⟶ Y) [IsClosedImmersion g] :
    g ⁻¹ᵁ ActualOpenSupport.complement g = ⊥ := by
…

    Mentions: OAI.ActualOpenSupport.complement

  13. lemma OAI.ActualCartier.coherent_power_tensor_line line 253

    Source documentation

    All powers of the Cartier ideal preserve coherence.

    lemma coherent_power_tensor_line (L : Y.Modules)
    (d : LineTrivialization Y.sheaf L) (n : ℕ)
    (M : Y.Modules) [M.IsFinitePresentation] :
    ((power (tensorLeft Y.sheaf L) n).obj M).IsFinitePresentation := by
…
  14. lemma OAI.ActualCartier.cleared_extension_puncture_isIso line 264

    Source documentation

    A global extension retaining a puncture identification is an isomorphism on the puncture.

    lemma cleared_extension_puncture_isIso (g : X ⟶ Y) [IsClosedImmersion g]
    (M N : Y.Modules) (n : ℕ)
    (e : M.over (ActualOpenSupport.complement g) ≅ N.over (ActualOpenSupport.complement g))
    (a : (power (tensorLeft Y.sheaf (idealSheaf g)) n).obj M ⟶ N)
    (ha : a.over (ActualOpenSupport.complement g) =
      ((powerAction (tensorLeft Y.sheaf (idealSheaf g))
        (idealAction Y.sheaf (idealι g)) n).app M).over (ActualOpenSupport.complement g) ≫ e.hom) :
    IsIso ((restrictFunctor (ActualOpenSupport.complement g).ι).map a) := by
…

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

  15. lemma OAI.ActualCartier.exists_global_cleared_extension_of_local_bounds line 300

    Source documentation

    The local-to-global part of coherent denominator clearing, with the ideal twist and the geometric puncture. Local bounds are uniformized, overlap compatibility is proved by torsion freeness, maps are glued, and the resulting cokernel is supported on the divisor. The local extension property itself must still be supplied, for instance by transporting the proved affine denominator-clearing theorem.

    lemma exists_global_cleared_extension_of_local_bounds
    {ι : Type*} [Fintype ι] (U : ι → Y.Opens) (hU : (⨆ i, U i) = ⊤)
    (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ≅
      N.over (ActualOpenSupport.complement g))
    (hloc : ∀ i, ∃ k : ℕ, ∀ n : ℕ, k ≤ n →
      ∃ a : ((power (tensorLeft Y.sheaf (idealSheaf g)) n).obj M).over (U i) ⟶ N.over (U i),
        Mono a ∧ ∀ (V : Y.Opens) (hi : V ≤ U i)
          (hV : V ≤ ActualOpenSupport.complement g)
          (x : ((power (tensorLeft Y.sheaf (idealSheaf g)) n).obj M).val.obj (op V)),
          a.val.app (op (Over.mk (homOfLE hi))) x =
…

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

  16. def OAI.ActualOpenModules.isoRestrictEquiv line 346

    Source documentation

    Restriction along a scheme isomorphism is an equivalence of its module sheaf categories.

    def isoRestrictEquiv (e : X ≅ Y) : Y.Modules ≌ X.Modules :=
…
  17. def OAI.ActualOpenModules.chartEquiv line 355

    Source documentation

    The modules on any open-immersion chart are exactly the modules on the target's slice site at its image open.

    def chartEquiv (f : X ⟶ Y) [IsOpenImmersion f] :
    SheafOfModules (Y.ringCatSheaf.over f.opensRange) ≌ X.Modules :=
…
  18. def OAI.ActualOpenModules.chartRestrictionIso line 360

    Source documentation

    The chart equivalence intertwines global restriction with slice-site restriction.

    def chartRestrictionIso (f : X ⟶ Y) [IsOpenImmersion f] :
    SheafOfModules.overFunctor Y.ringCatSheaf f.opensRange ⋙ (chartEquiv f).functor ≅
      restrictFunctor f :=
…

    Mentions: OAI.ActualOpenModules.chartEquiv

  19. def OAI.ActualOpenModules.chartMap line 368

    Source documentation

    Transfer a chart morphism to the target slice site by the fully faithful inverse.

    def chartMap (f : X ⟶ Y) [IsOpenImmersion f] {M N : Y.Modules}
    (a : (restrictFunctor f).obj M ⟶ (restrictFunctor f).obj N) :
    M.over f.opensRange ⟶ N.over f.opensRange :=
…
  20. lemma OAI.ActualOpenModules.chartMap_fac line 374
  21. lemma OAI.ActualOpenModules.chartMap_mono line 380
  22. lemma OAI.ActualOpenModules.chartMap_restrict line 387

    Source documentation

    Transferring a restricted global morphism recovers its slice-site restriction.

    lemma chartMap_restrict (f : X ⟶ Y) [IsOpenImmersion f] {M N : Y.Modules}
    (a : M ⟶ N) : chartMap f ((restrictFunctor f).map a) = a.over f.opensRange := by
…

    Mentions: OAI.ActualOpenModules.chartMap

  23. lemma OAI.ActualOpenModules.image_eq line 403
  24. lemma OAI.ActualOpenModules.over_hom_component line 407
  25. lemma OAI.ActualOpenModules.over_inv_component line 410
  26. lemma OAI.ActualOpenModules.restrict_map_component line 413
  27. lemma OAI.ActualOpenModules.over_hom_eq line 417
  28. lemma OAI.ActualOpenModules.restrict_map_eq line 419
  29. lemma OAI.ActualOpenModules.module_associator_component line 423
  30. lemma OAI.ActualOpenModules.chart_object line 427
  31. lemma OAI.ActualOpenModules.chartRestriction_hom_apply line 433
  32. lemma OAI.ActualOpenModules.chartMap_fac_hom line 453
  33. lemma OAI.ActualOpenModules.chartFunctor_apply line 464
  34. lemma OAI.ActualOpenModules.raw_comp_apply line 470
  35. lemma OAI.ActualOpenModules.raw_chartRestriction_hom_apply line 474
  36. lemma OAI.ActualOpenModules.chartMap_relation line 480
  37. lemma OAI.ActualOpenModules.over_eq_naturality line 498
  38. lemma OAI.ActualOpenModules.eq_map_cancel line 508
  39. lemma OAI.ActualOpenModules.chartMap_apply line 516
  40. lemma OAI.ActualOpenModules.component_eq_transport line 538
  41. lemma OAI.ActualOpenModules.chartMap_puncture_compat line 552

    Source documentation

    Chart transport preserves the fixed morphism on every open in the geometric puncture.

    lemma chartMap_puncture_compat {M N : Y.Modules} (W : Y.Opens)
    (a : (restrictFunctor f).obj M ⟶ (restrictFunctor f).obj N)
    (b : M.over W ⟶ N.over W)
    (hab : a.over (f ⁻¹ᵁ W) =
      ActualOpenComparison.pullOverHom f (f ⁻¹ᵁ W) W (f.image_preimage_le W) b)
    (V : Y.Opens) (hi : V ≤ f.opensRange) (hV : V ≤ W)
    (x : M.val.obj (op V)) :
    (chartMap f a).val.app (op (Over.mk (homOfLE hi))) x =
      b.val.app (op (Over.mk (homOfLE hV))) x := by
…

    Mentions: OAI.ActualOpenComparison.pullOverHom, OAI.ActualOpenModules.chartMap

  42. lemma OAI.ActualCartier.exists_global_cleared_extension line 582

    Source documentation

    Global coherent denominator clearing along the Cartier ideal uses finite affine bounds and agreement on overlaps.

    lemma exists_global_cleared_extension
    (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hM : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (M.val.obj V))
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ≅
      N.over (ActualOpenSupport.complement g)) :
    ∃ k : ℕ, ∀ n : ℕ, k ≤ n →
      ∃ a : (power (tensorLeft Y.sheaf (idealSheaf g)) n).obj M ⟶ N,
        Mono a ∧
        a.over (ActualOpenSupport.complement g) =
          ((powerAction (tensorLeft Y.sheaf (idealSheaf g))
            (idealAction Y.sheaf (idealι g)) n).app M).over (ActualOpenSupport.complement g) ≫ e.hom ∧
…

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

  43. lemma OAI.ActualCartier.exists_global_power_sandwich line 613

    Source documentation

    The two-sided global Cartier lattice sandwich uses one bound for every larger power and retains the fixed puncture identification.

    lemma exists_global_power_sandwich
    (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hM : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (M.val.obj V))
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ≅
      N.over (ActualOpenSupport.complement g)) :
    let T := tensorLeft Y.sheaf (idealSheaf g)
…

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

  44. lemma OAI.ActualCartier.embedding_puncture_identity line 651

    Source documentation

    A lattice embedding gives the divisor Grothendieck identity. Torsion freeness descends from the target, and the cokernel supplies the finite filtration by supported layers.

    lemma embedding_puncture_identity {M N : Coh Y} (a : M ⟶ N) [Mono a]
    (hN : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (N.obj.val.obj U))
    [IsIso ((restrictFunctor (ActualOpenSupport.complement g).ι).map
      ((cohInclusion Y).map a))] :
    ∃ n : ℕ, cls ((restriction g d).obj M) = cls ((restriction g d).obj N) +
      ((idealLayers g d n (cokernel a)).map fun Q =>
        cls (conormalTensor g d Q) - cls Q).sum := by
…

    Mentions: OAI.ActualOpenSupport.complement, OAI.ActualCartier.restriction, OAI.ActualCartier.idealLayers, OAI.ActualCartier.conormalTensor

  45. lemma OAI.ActualCartier.module_embedding_puncture_identity line 664

    Source documentation

    The divisor identity for a denominator-cleared morphism of coherent module sheaves.

    lemma module_embedding_puncture_identity (M N : Y.Modules)
    [M.IsFinitePresentation] [N.IsFinitePresentation] (a : M ⟶ N) [Mono a]
    (hN : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (N.val.obj U))
    [IsIso ((restrictFunctor (ActualOpenSupport.complement g).ι).map a)] :
    let M' : Coh Y := ⟨M, inferInstance⟩
…

    Mentions: OAI.ActualOpenSupport.complement

  46. def OAI.ActualCartier.clearedLattice line 701

    Source documentation

    The coherent sheaf obtained by twisting a coherent lattice by a nonnegative Cartier ideal power.

    def clearedLattice (n : ℕ) (M : Y.Modules) [M.IsFinitePresentation] : Coh Y :=
…
  47. lemma OAI.ActualCartier.exists_cleared_lattice_identity line 707

    Source documentation

    Lattices identified off the divisor give a finite quotient filtration, epimorphisms from conormal twists, and the divisor Grothendieck identity.

    lemma exists_cleared_lattice_identity
    (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

  48. def OAI.CartierImageFiltration.powerAddIso line 763

    Source documentation

    Reassociate ideal powers without changing their order.

    def powerAddIso (n : ℕ) : (m : ℕ) → (M : C) →
    (power T (n + m)).obj M ≅ (power T n).obj ((power T m).obj M)
  | 0, _ => Iso.refl _
  | m + 1, M => powerAddIso n m (T.obj M)

/-- The action of an added power is the composite of the two power actions, with the canonical reassociation included. -/

    Mentions: OAI.CartierImageFiltration.power

  49. lemma OAI.CartierImageFiltration.powerAction_add line 769

    Source documentation

    The action of an added power is the composite of the two power actions, with the canonical reassociation included.

    lemma powerAction_add (m n : ℕ) (M : C) :
    (powerAddIso T n m M).hom ≫
        (powerAction T a n).app ((power T m).obj M) ≫
          (powerAction T a m).app M = (powerAction T a (n + m)).app M := by
…

    Mentions: OAI.CartierImageFiltration.powerAddIso, OAI.CartierImageFiltration.powerAction, OAI.CartierImageFiltration.power

  50. lemma OAI.CartierImageFiltration.power_sandwich_map line 786

    Source documentation

    A pair of maps that is inverse after restricting the puncture gives a power-action factorization there, including the canonical power reassociation. This is the functorial calculation for the Cartier sandwich.

    lemma power_sandwich_map {D : Type*} [Category D] (F : C ⥤ D)
    (n : ℕ) {M N : C} (e : F.obj M ≅ F.obj N)
    (f : (power T n).obj M ⟶ N) (g : (power T n).obj N ⟶ M)
    (hf : F.map f = F.map ((powerAction T a n).app M) ≫ e.hom)
    (hg : F.map g = F.map ((powerAction T a n).app N) ≫ e.inv) :
    F.map ((powerAddIso T n n N).hom ≫ (power T n).map g ≫ f) =
      F.map ((powerAction T a (n + n)).app N) := by
…

    Mentions: OAI.CartierImageFiltration.power, OAI.CartierImageFiltration.powerAction, OAI.CartierImageFiltration.powerAddIso