CoherentGlobalHom.lean`

52 declarations, 0 contain sorry, 0 declared as axioms

A direct algebraic proof of the torsion-free divisor restriction of a dual, used for the reflexive extension in the manuscript, lines 326–342.

def OAI.CoherentDual.globalHomEquiv line 16
abbrev OAI.CoherentDual.affineHom line 51
def OAI.CoherentDual.affineHomLinearMap line 53
lemma OAI.CoherentDual.affineHomLinearMap_global line 72
lemma OAI.CoherentDual.affineHomLinearMap_bijective line 88
def OAI.CoherentDual.affineHomLinearEquiv line 110
Source documentation
The global sections of the actual affine internal Hom are precisely the module Hom, as modules, not merely as abstract sets.
```
def affineHomLinearEquiv :
    (moduleSpecΓFunctor.obj (affineHom M N)) ≃ₗ[A] (M →ₗ[A] N) :=
…
```
Mentions: OAI.CoherentDual.affineHom
lemma OAI.CoherentGlobal.coherent_kernel_free_over line 125
lemma OAI.CoherentDual.coherent_dual_over_of_presentation line 156
def OAI.CoherentDual.overLocalForward line 196
def OAI.CoherentDual.overLocalBackward line 202
instance OAI.CoherentDual.overLocalModule line 208
def OAI.CoherentDual.overLocalEquiv line 217
Source documentation
Restriction of local linear Hom to a slice is the local linear Hom on that slice. This is the actual restriction identity needed to glue coherence.
```
def overLocalEquiv (V : Over U) :
    linearLocalHom (R := R) (M := M) (N := N) V.left ≃ₗ[R.obj (op V.left)]
…
```
Mentions: OAI.CoherentDual.linearLocalHom
def OAI.CoherentDual.homOverPresheafIso line 256
def OAI.CoherentDual.homOverIso line 273
Source documentation
Internal Hom commutes with actual restriction to the slice site.
```
def homOverIso :
    (homSheaf R₁ M₁ N₁).over U ≅ homSheaf (R₁.over U) (M₁.over U) (N₁.over U) := by
…
```
Mentions: OAI.CoherentDual.homSheaf
lemma OAI.CoherentDual.coherent_dual line 283
Source documentation
The actual internal structure-sheaf dual of a coherent sheaf on a locally Noetherian scheme is coherent.
```
lemma coherent_dual {X : Scheme.{0}} [IsLocallyNoetherian X]
    (M : X.Modules) [M.IsFinitePresentation] :
    (homSheaf X.sheaf M (SheafOfModules.unit _)).IsFinitePresentation := by
…
```
Mentions: OAI.CoherentDual.homSheaf

lemma OAI.CoherentDual.coherent_doubleDual line 298

Source documentation

The double dual in the model construction is an actual coherent sheaf.

lemma coherent_doubleDual {X : Scheme.{0}} [IsLocallyNoetherian X]
    (M : X.Modules) [M.IsFinitePresentation] :
    (homSheaf X.sheaf (homSheaf X.sheaf M (SheafOfModules.unit _))
      (SheafOfModules.unit _)).IsFinitePresentation := by
…

Mentions: OAI.CoherentDual.homSheaf

lemma OAI.CoherentPullback.exists_presentation_tilde line 315

lemma OAI.CoherentPullback.exists_presentation_pullback line 332

Source documentation

Pullback carries an actual finite global presentation to one.

lemma exists_presentation_pullback {X Y : Scheme} (f : X ⟶ Y)
    {M : Y.Modules} (P : M.Presentation) [P.IsFinite] :
    ∃ Q : ((Scheme.Modules.pullback f).obj M).Presentation, Q.IsFinite := by
…

lemma OAI.CoherentPullback.exists_presentation_pullback_tilde line 365

Source documentation

The actual sheaf p^*(M^~) used in the manuscript, lines 328 has a global finite presentation, for any scheme model over a Noetherian affine.

lemma exists_presentation_pullback_tilde {A : CommRingCat.{0}} [IsNoetherianRing A]
    {X : Scheme} (p : X ⟶ Spec A) (M : ModuleCat A) [Module.Finite A M] :
    ∃ P : ((Scheme.Modules.pullback p).obj (tilde M)).Presentation, P.IsFinite := by
…

abbrev OAI.CoherentModelActual.E line 377
Source documentation
The exact double-dual construction in the manuscript, lines 328.
```
abbrev E {A : CommRingCat.{0}} {W : Scheme.{0}} (p : W ⟶ Spec A) (M : ModuleCat A) : W.Modules :=
…
```

lemma OAI.CoherentModelActual.coherent_E line 383

Source documentation

The model sheaf is coherent for every finite module.

lemma coherent_E {A : CommRingCat.{0}} [IsNoetherianRing A] {W : Scheme.{0}}
    [IsLocallyNoetherian W] (p : W ⟶ Spec A) (M : ModuleCat A) [Module.Finite A M] :
    (E p M).IsFinitePresentation := by
…

Mentions: OAI.CoherentModelActual.E

def OAI.CoherentDual.affineDualGammaIso line 404
def OAI.CoherentDual.affineDualIso line 411
Source documentation
The affine sheaf dual is the associated sheaf of the actual module dual. Coherence, rather than a blanket Hom/localization assumption, supplies the counit isomorphism.
```
def affineDualIso : tilde (ModuleCat.of A (Module.Dual A M)) ≅
    homSheaf (Spec A).sheaf (tilde M) (SheafOfModules.unit _) := by
…
```
Mentions: OAI.CoherentDual.homSheaf
def OAI.AffinePullback.pushforwardGammaIso line 443
Source documentation
Global sections of pushforward along an affine map are scalar restriction.
```
def pushforwardGammaIso :
    pushforward (Spec.map f) ⋙ (moduleSpecΓFunctor (R := A)) ≅
…
```
def OAI.AffinePullback.pullbackTildeIso line 451
Source documentation
Affine pullback of an associated module is the actual tensor-product extension of scalars, obtained by uniqueness of adjoints.
```
def pullbackTildeIso :
    tilde.functor A ⋙ pullback (Spec.map f) ≅
      ModuleCat.extendScalars f.hom ⋙ tilde.functor B :=
…
```
def OAI.AffinePullback.pushforwardTildeIso line 466
Source documentation
The actual pushforward of an associated sheaf along an affine morphism is the associated sheaf of scalar restriction.
```
def pushforwardTildeIso (M : ModuleCat B) :
    (Scheme.Modules.pushforward (Spec.map f)).obj (tilde M) ≅
      tilde ((ModuleCat.restrictScalars f.hom).obj M) := by
…
```
def OAI.DualCartierRestriction.tDual line 489
lemma OAI.DualCartierRestriction.mem_tDual_iff line 492
lemma OAI.DualCartierRestriction.regular_on_restriction line 522
Source documentation
A dual restricted to a prime effective Cartier divisor is torsion-free. This is phrased in terms of scalars in R, without assuming an extra action of the quotient ring.
```
lemma regular_on_restriction (t : R) (ht : IsSMulRegular R t)
    [hprime : (Ideal.span ({t} : Set R)).IsPrime] (r : R)
    (hr : r ∉ Ideal.span ({t} : Set R)) :
    IsSMulRegular (Module.Dual R M ⧸ tDual (M := M) t) r := by
…
```
Mentions: OAI.DualCartierRestriction.tDual
lemma OAI.DualCartierRestriction.killed_by_equation line 532
instance OAI.DualCartierRestriction.quotientModule line 538
lemma OAI.DualCartierRestriction.torsionFree_restriction line 542
lemma OAI.DualCartierRestriction.tDual_eq_span_smul line 561
def OAI.DualCartierRestriction.tensorRestrictionEquiv line 570
Source documentation
The module-theoretic pullback of a dual to a principal divisor is the canonical quotient of that dual.
```
def tensorRestrictionEquiv (t : R) :
    ((R ⧸ Ideal.span ({t} : Set R)) ⊗[R] Module.Dual R M) ≃ₗ[R]
      Module.Dual R M ⧸ tDual (M := M) t :=
…
```
Mentions: OAI.DualCartierRestriction.tDual
lemma OAI.DualCartierRestriction.tensorRestrictionEquiv_mk_smul line 576

def OAI.DualCartierRestriction.tensorRestrictionQuotientEquiv line 585

Source documentation

Quotient-linearity of the affine pullback/quotient identification.

def tensorRestrictionQuotientEquiv (t : R) :
    ((R ⧸ Ideal.span ({t} : Set R)) ⊗[R] Module.Dual R M) ≃ₗ[R ⧸ Ideal.span ({t} : Set R)]
      Module.Dual R M ⧸ tDual (M := M) t where
…

Mentions: OAI.DualCartierRestriction.tDual

lemma OAI.DualCartierRestriction.torsionFree_tensorRestriction line 595

Source documentation

Actual tensor-product restriction of any dual to an integral effective Cartier divisor is torsion-free over the divisor ring.

lemma torsionFree_tensorRestriction (t : R) (ht : IsSMulRegular R t)
    [(Ideal.span ({t} : Set R)).IsPrime] :
    Module.IsTorsionFree (R ⧸ Ideal.span ({t} : Set R))
      ((R ⧸ Ideal.span ({t} : Set R)) ⊗[R] Module.Dual R M) := by
…

def OAI.CoherentDual.affineDualPullbackIso line 617

Source documentation

A concrete affine restriction of the actual sheaf dual, with the actual scalar-extension module, rather than a substitute quotient object.

def affineDualPullbackIso (f : A ⟶ B) :
    (Scheme.Modules.pullback (Spec.map f)).obj
      (homSheaf (Spec A).sheaf (tilde M) (SheafOfModules.unit _)) ≅
      tilde ((ModuleCat.extendScalars f.hom).obj (ModuleCat.of A (Module.Dual A M))) :=
…

Mentions: OAI.CoherentDual.homSheaf

def OAI.CoherentDual.affineDualPullbackGammaIso line 626

Source documentation

Global sections of affine pullback of the sheaf dual are the tensor extension of the module dual, as modules over the target ring.

def affineDualPullbackGammaIso (f : A ⟶ B) :
    moduleSpecΓFunctor.obj ((Scheme.Modules.pullback (Spec.map f)).obj
      (homSheaf (Spec A).sheaf (tilde M) (SheafOfModules.unit _))) ≅
      (ModuleCat.extendScalars f.hom).obj (ModuleCat.of A (Module.Dual A M)) :=
…

Mentions: OAI.CoherentDual.homSheaf

lemma OAI.CoherentDual.affineDualPullbackGamma_torsionFree line 635
Source documentation
The actual sheaf-dual restriction has torsion-free affine sections along an integral effective Cartier divisor (the manuscript, lines 326–342).
```
lemma affineDualPullbackGamma_torsionFree (t : A) (ht : IsSMulRegular A t)
    [(Ideal.span ({t} : Set A)).IsPrime] :
    let f : A ⟶ CommRingCat.of (A ⧸ Ideal.span ({t} : Set A)) :=
…
```
abbrev OAI.CoherentModelActual.affineModule line 666
Source documentation
The actual scalar-extension module on an affine model chart.
```
abbrev affineModule := (ModuleCat.extendScalars f.hom).obj M
```
instance OAI.CoherentModelActual.affineModule_finite line 668
instance OAI.CoherentModelActual.affineModule_dual_finite line 673
def OAI.CoherentModelActual.affineFirstDualIso line 680
Source documentation
The first sheaf dual of the actual pullback is the associated module dual of the actual tensor extension, not an abstract reflexive object.
```
def affineFirstDualIso :
    tilde (ModuleCat.of B (Module.Dual B (affineModule f M))) ≅
      homSheaf (Spec B).sheaf ((Scheme.Modules.pullback (Spec.map f)).obj (tilde M))
        (SheafOfModules.unit _) :=
…
```
Mentions: OAI.CoherentModelActual.affineModule
def OAI.CoherentModelActual.affineEIso line 689
Source documentation
The affine description of the precise double-dual model extension.
```
def affineEIso : E (Spec.map f) M ≅
    tilde (ModuleCat.of B (Module.Dual B (Module.Dual B (affineModule f M)))) :=
…
```
Mentions: OAI.CoherentModelActual.E, OAI.CoherentModelActual.affineModule
theorem OAI.CoherentModelActual.affineE_cartier_torsionFree line 698
Source documentation
Restricting the genuine affine model extension to an integral Cartier divisor gives torsion-free sections. Only the literal regular equation and primality are used; the model sheaf is CONSTRUCTED from arbitrary M.
```
theorem affineE_cartier_torsionFree (t : B) (ht : IsSMulRegular B t)
    [(Ideal.span ({t} : Set B)).IsPrime] :
    let q : B ⟶ CommRingCat.of (B ⧸ Ideal.span ({t} : Set B)) :=
…
```
lemma OAI.FiniteDomainDual.exists_dual_ne_zero line 737
Source documentation
A finite presented torsion-free module over a domain has enough honest R-valued dual functionals. Denominators are cleared over R, not assumed away.
```
lemma exists_dual_ne_zero [Module.FinitePresentation R M] [Module.IsTorsionFree R M]
    {m : M} (hm : m ≠ 0) : ∃ f : Module.Dual R M, f m ≠ 0 := by
…
```
lemma OAI.FiniteDomainDual.dual_nontrivial line 768
Source documentation
Nontriviality of the dual is derived, rather than built into the model sheaf input.
```
lemma dual_nontrivial [Module.FinitePresentation R M] [Module.IsTorsionFree R M]
    [Nontrivial M] : Nontrivial (Module.Dual R M) := by
…
```

lemma OAI.FiniteDomainDual.doubleDual_baseChange_nontrivial line 777

Source documentation

Even non-flat birational base change does not kill the double dual of a nonzero finite torsion-free module. The ring-map injectivity is essential; no flatness of the blowup chart is asserted.

lemma doubleDual_baseChange_nontrivial [Module.FinitePresentation R M]
    [Module.IsTorsionFree R M] [Nontrivial M]
    (B : Type*) [CommRing B] [Algebra R B]
    (hinj : Function.Injective (algebraMap R B)) :
    Nontrivial (Module.Dual B (Module.Dual B (B ⊗[R] M))) := by
…

lemma OAI.FiniteDomainDual.mem_support line 791
Source documentation
Every prime is in the support of a nonzero torsion-free module over a domain.
```
lemma mem_support [Module.IsTorsionFree R M] [Nontrivial M] (p : PrimeSpectrum R) :
    p ∈ Module.support R M := by
…
```
lemma OAI.FiniteDomainDual.prime_fiber_nontrivial line 801
Source documentation
A finite, nonzero torsion-free module remains nonzero on every prime fiber; this supplies the positivity lost by a mere torsion-free assertion.
```
lemma prime_fiber_nontrivial [Module.Finite R M] [Module.IsTorsionFree R M]
    [Nontrivial M] (p : Ideal R) [p.IsPrime] :
    Nontrivial ((R ⧸ p) ⊗[R] M) := by
…
```

lemma OAI.FiniteDomainDual.prime_fiber_rank_pos line 816

Source documentation

The actual generic rank of the prime-divisor restriction is positive. The residue field here is Mathlib's fraction field of R/p.

lemma prime_fiber_rank_pos [Module.Finite R M] [Module.IsTorsionFree R M]
    [Nontrivial M] (p : Ideal R) [p.IsPrime] :
    0 < Module.finrank p.ResidueField
      (p.ResidueField ⊗[R ⧸ p] ((R ⧸ p) ⊗[R] M)) := by
…