CartierEquation.lean`

60 declarations, 0 contain sorry, 0 declared as axioms

From regular affine equations to trivializations of the actual kernel ideal sheaf. This is needed to construct the source Cartier data.

theorem OAI.ActualCartier.kernelMono line 39
abbrev OAI.ActualCartier.SectionTrivialization line 46
Source documentation
A trivialization of the section module of the ideal.
```
abbrev SectionTrivialization :=
…
```
def OAI.ActualCartier.equation line 51
lemma OAI.ActualCartier.equation_mem_kernel line 53
lemma OAI.ActualCartier.equation_regular line 59
lemma OAI.ActualCartier.kernel_eq_span_equation line 86
Source documentation
The closed ideal is generated by the regular local equation extracted from its trivialization. Neither principality nor regularity is an extra hypothesis about the section-ring map.
```
lemma kernel_eq_span_equation :
    RingHom.ker (f.app U).hom = Ideal.span ({equation f U e} : Set Γ(Y, U)) := by
…
```
Mentions: OAI.ActualCartier.equation
def OAI.ActualCartier.lineSectionTrivialization line 107
Source documentation
Slice-site line trivializations induce section-module trivializations on Cartier charts.
```
def lineSectionTrivialization (d : LineTrivialization Y.sheaf (idealSheaf f)) (i : d.I) :
    SectionTrivialization f (d.obj i) :=
…
```
Mentions: OAI.ActualCartier.idealSheaf, OAI.ActualCartier.SectionTrivialization

lemma OAI.SheafTorsion.of_cover line 122

Source documentation

Torsion freedom of sections on an integral scheme is local on an arbitrary open cover. Empty intersections are included, via the zero section ring.

lemma of_cover {X : Scheme.{0}} [IsIntegral X] (M : X.Modules)
    {ι : Type*} (U : ι → X.Opens) (hU : (⨆ i, U i) = ⊤)
    (hM : ∀ i (V : X.Opens), V ≤ U i →
      Module.IsTorsionFree Γ(X, V) (M.val.obj (op V)))
    (W : X.Opens) : Module.IsTorsionFree Γ(X, W) (M.val.obj (op W)) where
…

lemma OAI.SheafTorsion.tensor_line line 162

Source documentation

Twisting a torsion-free module sheaf by a line bundle preserves torsion freedom. No formal 'twist' operation is assumed.

lemma tensor_line {X : Scheme.{0}} [IsIntegral X] (L N : X.Modules)
    (d : LineTrivialization X.sheaf L)
    (hN : ∀ U, Module.IsTorsionFree (X.sheaf.obj.obj U) (N.val.obj U))
    (U : X.Opensᵒᵖ) :
    Module.IsTorsionFree (X.sheaf.obj.obj U) ((tensor X.sheaf L N).val.obj U) := by
…

lemma OAI.SheafTorsion.regular_ringEquiv line 188

lemma OAI.SheafTorsion.restrict line 202

Source documentation

Sectionwise torsion freedom survives open-scheme restriction, including the coefficient-ring isomorphism in that restriction.

lemma restrict {X Y : Scheme.{0}} (f : X ⟶ Y) [IsOpenImmersion f]
    (M : Y.Modules)
    (hM : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (M.val.obj U))
    (U : X.Opensᵒᵖ) : Module.IsTorsionFree (X.sheaf.obj.obj U)
      (((restrictFunctor f).obj M).val.obj U) := by
…

lemma OAI.SheafTorsion.of_restrict line 217

Source documentation

Conversely, torsion freedom of restricted sections gives torsion freedom over the original coefficient ring on the image open.

lemma of_restrict {X Y : Scheme.{0}} (f : X ⟶ Y) [IsOpenImmersion f]
    (M : Y.Modules) (U : X.Opens)
    [Module.IsTorsionFree Γ(X, U) (((restrictFunctor f).obj M).val.obj (op U))] :
    Module.IsTorsionFree Γ(Y, f ''ᵁ U) (M.val.obj (op (f ''ᵁ U))) := by
…

lemma OAI.SheafTorsion.of_restrict_cover line 232

Source documentation

Local torsion freedom on an open immersion cover is a global property of the sheaf, without identifying non-definitional section rings.

lemma of_restrict_cover {X : Scheme.{0}} [IsIntegral X] (M : X.Modules)
    {ι : Type*} (U : ι → X.Opens) (hU : (⨆ i, U i) = ⊤)
    (hM : ∀ i V, Module.IsTorsionFree ((U i).toScheme.sheaf.obj.obj V)
      (((restrictFunctor (U i).ι).obj M).val.obj V))
    (W : X.Opens) : Module.IsTorsionFree Γ(X, W) (M.val.obj (op W)) := by
…

lemma OAI.SheafTorsion.of_restrict_iso line 259

Source documentation

Torsion freedom can be reflected through an scheme isomorphism, without treating the two structure sheaves as definitionally equal.

lemma of_restrict_iso {X Y : Scheme.{0}} (f : X ⟶ Y) [IsIso f] (M : Y.Modules)
    (hM : ∀ U, Module.IsTorsionFree (X.sheaf.obj.obj U)
      (((restrictFunctor f).obj M).val.obj U))
    (V : Y.Opensᵒᵖ) : Module.IsTorsionFree (Y.sheaf.obj.obj V) (M.val.obj V) := by
…

def OAI.CoherentDual.pullbackIsoSpec line 284

Source documentation

Pullback comparison for the affine identifications of source and target, retaining the map of global section rings.

def pullbackIsoSpec (N : Y.Modules) :
    (restrictFunctor X.isoSpec.inv).obj ((Scheme.Modules.pullback f).obj N) ≅
      (Scheme.Modules.pullback (Spec.map f.appTop)).obj
        ((restrictFunctor Y.isoSpec.inv).obj N) :=
…

lemma OAI.CoherentDual.affineSchemeDual_restriction_torsionFree line 298

Source documentation

Dual restriction to a closed integral Cartier subscheme of an affine scheme is torsion-free. Its regular defining equation is derived from the given trivialization of the kernel ideal, not added as a hypothesis.

lemma affineSchemeDual_restriction_torsionFree
    [IsLocallyNoetherian Y] [IsIntegral X] [IsClosedImmersion f]
    (e : ActualCartier.SectionTrivialization f ⊤)
    (M : Y.Modules) [M.IsFinitePresentation]
    (U : X.Opensᵒᵖ) : Module.IsTorsionFree (X.sheaf.obj.obj U)
      (((Scheme.Modules.pullback f).obj
        (homSheaf Y.sheaf M (SheafOfModules.unit _))).val.obj U) := by
…

Mentions: OAI.ActualCartier.SectionTrivialization, OAI.CoherentDual.homSheaf

def OAI.ActualCartier.structureTargetRestrictIso line 335

Source documentation

The pushed-forward structure sheaf has the canonical open base-change identification.

def structureTargetRestrictIso :
    (restrictFunctor U.ι).obj ((pushforward f).obj (SheafOfModules.unit _)) ≅
      (pushforward (f ∣_ U)).obj (SheafOfModules.unit _) :=
…

lemma OAI.ActualCartier.structureMap_restrict line 341
def OAI.ActualCartier.idealRestrictionIso line 358
Source documentation
The kernel ideal of the closed morphism commutes with actual restriction, by preservation of kernels and the structure-map square.
```
def idealRestrictionIso :
    (restrictFunctor U.ι).obj (idealSheaf f) ≅ idealSheaf (f ∣_ U) :=
…
```
Mentions: OAI.ActualCartier.idealSheaf

def OAI.CoherentDual.dualPullbackRestrictIso line 375

Source documentation

Dual pullback restricted to an open of the target.

def dualPullbackRestrictIso (V : Y.Opens) (M : Y.Modules) :
    (restrictFunctor (f ⁻¹ᵁ V).ι).obj
      ((Scheme.Modules.pullback f).obj (homSheaf Y.sheaf M (SheafOfModules.unit _))) ≅
    (Scheme.Modules.pullback (f ∣_ V)).obj
      (homSheaf V.toScheme.sheaf ((restrictFunctor V.ι).obj M) (SheafOfModules.unit _)) :=
…

Mentions: OAI.CoherentDual.homSheaf

lemma OAI.CoherentDual.torsionFree_of_empty_scheme line 383

lemma OAI.CoherentDual.dual_restriction_torsionFree_of_trivial_ideal line 395

Source documentation

If the closed ideal is trivial, the dual restriction is torsion-free on every open of an integral divisor. Affine equations are derived from that ideal, and empty preimages in the affine cover are treated separately.

lemma dual_restriction_torsionFree_of_trivial_ideal
    [IsLocallyNoetherian Y] [IsIntegral X] [IsClosedImmersion f]
    (e : ActualCartier.idealSheaf f ≅ SheafOfModules.unit Y.ringCatSheaf)
    (M : Y.Modules) [M.IsFinitePresentation] (U : X.Opensᵒᵖ) :
    Module.IsTorsionFree (X.sheaf.obj.obj U)
      (((Scheme.Modules.pullback f).obj
        (homSheaf Y.sheaf M (SheafOfModules.unit _))).val.obj U) := by
…

Mentions: OAI.ActualCartier.idealSheaf, OAI.CoherentDual.homSheaf

lemma OAI.CoherentDual.dual_restriction_torsionFree line 426

Source documentation

Restriction of a coherent dual to an integral effective Cartier divisor is torsion-free; this applies in particular to the model double dual.

lemma dual_restriction_torsionFree
    [IsLocallyNoetherian Y] [IsIntegral X] [IsClosedImmersion f]
    (d : LineTrivialization Y.sheaf (ActualCartier.idealSheaf f))
    (M : Y.Modules) [M.IsFinitePresentation] (U : X.Opensᵒᵖ) :
    Module.IsTorsionFree (X.sheaf.obj.obj U)
      (((Scheme.Modules.pullback f).obj
        (homSheaf Y.sheaf M (SheafOfModules.unit _))).val.obj U) := by
…

Mentions: OAI.ActualCartier.idealSheaf, OAI.CoherentDual.homSheaf

lemma OAI.ActualCartier.ideal_section_mem_kernel line 461
def OAI.ActualCartier.sectionToKernel line 468
lemma OAI.ActualCartier.sectionToKernel_bijective line 472
def OAI.ActualCartier.sectionKernelEquiv line 486
lemma OAI.ActualCartier.idealSheaf_coherent line 490
def OAI.ActualCartier.affineIdealUnitIso line 502
Source documentation
On an affine target, a section-module trivialization produces a sheaf trivialization by the proved coherent affine equivalence.
```
def affineIdealUnitIso {A : CommRingCat.{0}} [IsNoetherianRing A]
    (f : X ⟶ Spec A) [IsClosedImmersion f] (e : SectionTrivialization f ⊤) :
    idealSheaf f ≅ SheafOfModules.unit (Spec A).ringCatSheaf := by
…
```
Mentions: OAI.ActualCartier.SectionTrivialization, OAI.ActualCartier.idealSheaf
def OAI.ActualCartier.principalIdealEquiv line 527
def OAI.ActualCartier.equationSectionTrivialization line 545
lemma OAI.ActualCartier.specMap_app_kernel line 550
lemma OAI.ActualCartier.specInverse_regular line 566
def OAI.ActualCartier.affinePrincipalIdealUnitIso line 577
def OAI.ActualCartier.chartSourceSectionsIso line 600
lemma OAI.ActualCartier.chart_section_square line 604
def OAI.ActualCartier.chartIdealSectionMap line 616
Source documentation
The kernel ideal on the chart, in its coefficient module.
```
def chartIdealSectionMap :
    ((restrictFunctor j).obj (idealSheaf f)).val.obj (op ⊤) →ₗ[Γ(Y', ⊤)]
      Γ(Y', ⊤) := by
…
```
Mentions: OAI.ActualCartier.idealSheaf
lemma OAI.ActualCartier.chartIdealSectionMap_apply line 626
lemma OAI.ActualCartier.chartIdealSectionMap_injective line 630
lemma OAI.ActualCartier.chartIdealSectionMap_mem line 637
def OAI.ActualCartier.chartIdealSectionToKernel line 650
lemma OAI.ActualCartier.chartIdealSectionToKernel_bijective line 655
def OAI.ActualCartier.chartIdealSectionsEquiv line 677
def OAI.ActualCartier.affineUnitIsoOfSections line 683
def OAI.ActualCartier.chartAffinePrincipalIdealUnitIso line 697
def OAI.ActualSheafTensor.lineTrivializationOfCharts line 716

def OAI.SourceExceptionalRestriction.chartIso line 756

Source documentation

Functoriality connects the global sheaf pullback with the actual regular quotient on each surface affine chart.

def chartIso (N : W.Modules) (i : Fin 3) :
    (restrictFunctor (surfaceIota i)).obj
      ((Scheme.Modules.pullback completedSourceZero).obj
        (homSheaf W.sheaf N (SheafOfModules.unit _))) ≅
    (Scheme.Modules.pullback (completedZeroChart i)).obj
      (homSheaf (Spec (.of (completedSourceChart i))).sheaf
        ((restrictFunctor (completedIota i)).obj N) (SheafOfModules.unit _)) :=
…

lemma OAI.SourceExceptionalRestriction.chart_torsionFree line 771

lemma OAI.SourceExceptionalRestriction.dual_restriction_torsionFree line 790

Source documentation

The global section modules of the exceptional restriction of any coherent dual are torsion-free over the integral surface.

lemma dual_restriction_torsionFree (N : W.Modules) [N.IsFinitePresentation]
    (U : ExplicitCone.projectiveSurface.Opens) :
    Module.IsTorsionFree Γ(ExplicitCone.projectiveSurface, U)
      (((Scheme.Modules.pullback completedSourceZero).obj
        (homSheaf W.sheaf N (SheafOfModules.unit _))).val.obj (op U)) := by
…

Mentions: OAI.ExplicitCone.projectiveSurface

abbrev OAI.SourceExceptionalRestriction.P line 809
lemma OAI.SourceExceptionalRestriction.P_torsionFree line 812
lemma OAI.CoherentPullback.coherent_from_affine line 834
lemma OAI.CoherentGlobal.weakSheafify_over line 849
lemma OAI.CoherentGlobal.wEqualsLocallyBijective_over line 853
lemma OAI.CoherentGlobal.coherent_of_iso line 859
Source documentation
Finite presentation is invariant under an isomorphism of module sheaves.
```
lemma coherent_of_iso {X : Scheme.{0}} {M N : X.Modules} (e : M ≅ N)
    (hM : M.IsFinitePresentation) : N.IsFinitePresentation :=
…
```

lemma OAI.CoherentGlobal.coherent_of_open_immersions line 864

Source documentation

Coherence descends along a covering family of open immersions.

lemma coherent_of_open_immersions {X : Scheme.{0}} {I : Type}
    {Y : I → Scheme.{0}} (f : ∀ i, Y i ⟶ X) [∀ i, IsOpenImmersion (f i)]
    (hcover : (⨆ i, (f i).opensRange) = ⊤) (M : X.Modules)
    (hM : ∀ i, ((restrictFunctor (f i)).obj M).IsFinitePresentation) :
    M.IsFinitePresentation := by
…

def OAI.SourceExceptionalRestriction.chartPullbackIso line 910
lemma OAI.SourceExceptionalRestriction.chart_pullback_coherent line 921
lemma OAI.SourceExceptionalRestriction.pullback_coherent line 929
lemma OAI.SourceExceptionalRestriction.P_coherent line 934