CoherentTensor.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CoherentModelActual.affineEPullbackGammaIso line 17
Source documentation
The actual section module of a restriction of the affine double-dual model extension, expressed as an honest scalar extension of the double dual.
```
def affineEPullbackGammaIso (q : B ⟶ C) :
    (moduleSpecΓFunctor (R := C)).obj
…
```
lemma OAI.CoherentModelActual.affineDoubleDual_nontrivial line 30
theorem OAI.CoherentModelActual.affineE_prime_restriction_nontrivial line 38
Source documentation
The arbitrary ungraded input module gives a NONZERO restriction of its literal affine model extension at every prime divisor.
```
theorem affineE_prime_restriction_nontrivial (hf : Function.Injective f)
    (p : Ideal B) [p.IsPrime] :
    let q : B ⟶ CommRingCat.of (B ⧸ p) := CommRingCat.ofHom (Ideal.Quotient.mk p)
…
```
theorem OAI.CoherentModelActual.affineE_cartier_rank_pos line 55
Source documentation
The restriction has strictly positive generic rank on the integral Cartier divisor. Positivity is deduced from M≠0, not assumed for the sheaf.
```
theorem affineE_cartier_rank_pos (hf : Function.Injective f)
    (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.CoherentDual.dual_sections_torsionFree line 93

Source documentation

Sections of an actual sheaf dual on an integral scheme are torsion-free. This does not postulate a torsion-free coherent object: it is proved pointwise on the local linear transformations defining the internal Hom.

lemma dual_sections_torsionFree {X : Scheme.{0}} [IsIntegral X]
    (M : X.Modules) (U : X.Opens) :
    @Module.IsTorsionFree Γ(X, U)
      ((homSheaf.{0,0,0,0} X.sheaf M (SheafOfModules.unit _)).val.obj (op U)) _ _
      ((homSheaf.{0,0,0,0} X.sheaf M (SheafOfModules.unit _)).val.obj (op U)).isModule := by
…

instance OAI.ModuleReindex.pushforwardZero_full line 146
Source documentation
Reindexing along an equivalence does not discard module morphisms. The linearity of the inverse natural transformation is transported through the counit isomorphism, rather than postulated.
```
instance pushforwardZero_full (F : C ⥤ D) [F.IsEquivalence]
    (R : Dᵒᵖ ⥤ RingCat.{u}) : (PresheafOfModules.pushforward₀.{u} F R).Full where
…
```
instance OAI.ModuleReindex.pushforwardZero_faithful line 172

instance OAI.ModuleReindex.restrictScalars_full line 180

Source documentation

Restriction through an isomorphism of the coefficient presheaves is full.

instance restrictScalars_full {R S : Cᵒᵖ ⥤ RingCat.{u}}
    (φ : R ⟶ S) [IsIso φ] : (PresheafOfModules.restrictScalars.{u} φ).Full where
…

def OAI.ModuleReindex.pushforward_fullyFaithful line 195

Source documentation

Actual reindexing plus coefficient isomorphism is fully faithful.

def pushforward_fullyFaithful (F : C ⥤ D) [F.IsEquivalence]
    {R : Dᵒᵖ ⥤ RingCat.{u}} {S : Cᵒᵖ ⥤ RingCat.{u}}
    (φ : S ⟶ F.op ⋙ R) [IsIso φ] :
    (PresheafOfModules.pushforward.{u} φ).FullyFaithful := by
…

def OAI.CoherentDual.homReindexApp line 218
lemma OAI.CoherentDual.homReindexApp_bijective line 235
def OAI.CoherentDual.homReindexPresheafIso line 254
Source documentation
Internal linear Hom is preserved by coefficient isomorphisms and a reindexing functor that is an equivalence on every slice.
```
def homReindexPresheafIso [IsIso φ]
    (hF : ∀ X, (Over.post (X := X) F).IsEquivalence) :
…
```
abbrev OAI.ActualSheafTensor.ringSheaf line 289
def OAI.ActualSheafTensor.tensor line 297
Source documentation
The actual tensor sheaf: sheafification of the objectwise tensor product of presheaves of modules. It will provide the Cartier line-bundle twists.
```
def tensor (M N : SheafOfModules.{u} (ringSheaf R)) : SheafOfModules.{u} (ringSheaf R) :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf
def OAI.ActualSheafTensor.tensorLeft line 301
Source documentation
Tensoring with a fixed sheaf, on both objects and morphisms.
```
def tensorLeft (M : SheafOfModules.{u} (ringSheaf R)) :
    SheafOfModules.{u} (ringSheaf R) ⥤ SheafOfModules.{u} (ringSheaf R) :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf
def OAI.ActualSheafTensor.leftUnitIso line 308
Source documentation
Tensoring the structure sheaf is canonically the identity, not a postulated operation on formal Chern data.
```
def leftUnitIso (M : SheafOfModules.{u} (ringSheaf R)) :
    tensor R (SheafOfModules.unit _) M ≅ M :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensor
def OAI.ActualSheafTensor.rightUnitIso line 314
Source documentation
The analogous canonical right unit isomorphism.
```
def rightUnitIso (M : SheafOfModules.{u} (ringSheaf R)) :
    tensor R M (SheafOfModules.unit _) ≅ M :=
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.tensor
def OAI.CoherentDual.tensorCurryAt line 335
Source documentation
A bilinear map of actual presheaves defines local linear maps by restricting its second argument.
```
def tensorCurryAt (f : M ⊗ N ⟶ P) (U : C) (y : N.obj (op U)) (V : Over U) :
    M.obj (op V.left) →+ P.obj (op V.left) where
…
```
def OAI.CoherentDual.tensorCurryLocal line 344
Source documentation
The sectionwise tensor-Hom adjunction on a slice.
```
def tensorCurryLocal (f : M ⊗ N ⟶ P) (U : C) (y : N.obj (op U)) :
    linearLocalHom (R := R) (M := M) (N := P) U := by
…
```
Mentions: OAI.CoherentDual.linearLocalHom
def OAI.CoherentDual.tensorCurryLinear line 367
def OAI.CoherentDual.tensorCurry line 397
Source documentation
Currying is a morphism of genuine presheaves of modules.
```
def tensorCurry (f : M ⊗ N ⟶ P) : N ⟶ homPresheaf (R := R) (M := M) (N := P) where
…
```
Mentions: OAI.CoherentDual.homPresheaf
def OAI.CoherentDual.tensorUncurryApp line 412
Source documentation
Evaluation gives the inverse to currying on each object.
```
def tensorUncurryApp (f : N ⟶ homPresheaf (R := R) (M := M) (N := P)) (U : Cᵒᵖ) :
…
```
Mentions: OAI.CoherentDual.homPresheaf
lemma OAI.CoherentDual.tensorUncurryApp_tmul line 430
def OAI.CoherentDual.tensorUncurry line 437
Source documentation
Uncurrying is compatible with restriction maps.
```
def tensorUncurry (f : N ⟶ homPresheaf (R := R) (M := M) (N := P)) : M ⊗ N ⟶ P where
…
```
Mentions: OAI.CoherentDual.homPresheaf
lemma OAI.CoherentDual.tensorUncurryCurry line 461
lemma OAI.CoherentDual.tensorCurryUncurry line 470
def OAI.CoherentDual.tensorHomEquiv line 486
Source documentation
Actual tensor-Hom equivalence for presheaves.
```
def tensorHomEquiv : (M ⊗ N ⟶ P) ≃ (N ⟶ homPresheaf (R := R) (M := M) (N := P)) where
…
```
Mentions: OAI.CoherentDual.homPresheaf
def OAI.CoherentDual.sheafTensorHomEquiv line 511
Source documentation
The tensor-Hom equivalence for actual module sheaves. The domain is the sheafification of the genuine sectionwise tensor product, and the codomain is the sheaf of local linear transformations proved to satisfy descent.
```
def sheafTensorHomEquiv :
    (ActualSheafTensor.tensor R M N ⟶ P) ≃ (N ⟶ homSheaf R M P) :=
…
```
Mentions: OAI.ActualSheafTensor.tensor, OAI.CoherentDual.homSheaf
lemma OAI.CoherentDual.tensorCurry_naturality_left line 518
lemma OAI.CoherentDual.sheafTensorHomEquiv_val line 534
lemma OAI.CoherentDual.sheafTensorHomEquiv_naturality_left line 542
def OAI.CoherentDual.tensorHomAdjunction line 560
Source documentation
Actual tensor sheaves are a left adjoint, so tensoring is right exact.
```
def tensorHomAdjunction : ActualSheafTensor.tensorLeft R M ⊣
    Adjunction.rightAdjointOfEquiv (F := ActualSheafTensor.tensorLeft R M) (fun N P => sheafTensorHomEquiv R M N P)
…
```
Mentions: OAI.ActualSheafTensor.tensorLeft, OAI.CoherentDual.sheafTensorHomEquiv
instance OAI.CoherentDual.tensorLeft_preservesColimits line 566
instance OAI.CoherentDual.opensPost_essSurj line 581
instance OAI.CoherentDual.opensPost_isEquivalence line 592

def OAI.CoherentDual.homSchemeRestrictionIso line 597

Source documentation

The actual internal linear Hom commutes with restriction to an open subscheme, including the non-definitional coefficient-ring isomorphism.

def homSchemeRestrictionIso {X Y : Scheme.{0}} (f : X ⟶ Y) [IsOpenImmersion f]
    (M N : Y.Modules) :
    (restrictFunctor f).obj (homSheaf Y.sheaf M N) ≅
      homSheaf X.sheaf ((restrictFunctor f).obj M) ((restrictFunctor f).obj N) := by
…

Mentions: OAI.CoherentDual.homSheaf

abbrev OAI.CoherentDual.homSheafCovFunctor line 608

Source documentation

Covariant functoriality in the target of the actual internal Hom.

abbrev homSheafCovFunctor {C : Type} [Category C] {J : GrothendieckTopology C}
    (R : Sheaf J CommRingCat.{0})
    [HasSheafify J AddCommGrpCat.{0}] [J.WEqualsLocallyBijective AddCommGrpCat.{0}]
    (M : SheafOfModules.{0} ((sheafCompose J (forget₂ CommRingCat RingCat)).obj R)) :=
…

def OAI.CoherentDual.dualSchemeRestrictionIso line 618

Source documentation

In particular the genuine coherent dual restricts to the genuine dual of the restricted sheaf; no formal identification of section rings is used.

def dualSchemeRestrictionIso {X Y : Scheme.{0}} (f : X ⟶ Y) [IsOpenImmersion f]
    (M : Y.Modules) :
    (restrictFunctor f).obj (homSheaf Y.sheaf M (SheafOfModules.unit _)) ≅
      homSheaf X.sheaf ((restrictFunctor f).obj M) (SheafOfModules.unit _) :=
…

Mentions: OAI.CoherentDual.homSheaf

def OAI.CoherentModelActual.doubleDualIso line 638

Source documentation

Functoriality of the literal structure-sheaf double dual.

def doubleDualIso {X : Scheme.{0}} {M N : X.Modules} (e : M ≅ N) :
    homSheaf X.sheaf (homSheaf X.sheaf M (SheafOfModules.unit _))
      (SheafOfModules.unit _) ≅
    homSheaf X.sheaf (homSheaf X.sheaf N (SheafOfModules.unit _))
      (SheafOfModules.unit _) :=
…

def OAI.CoherentModelActual.openPullbackEIso line 648
Source documentation
The global double-dual model is the actual double-dual model on EACH open affine chart. It is not an independently chosen local replacement.
```
def openPullbackEIso {A : CommRingCat.{0}} {V W : Scheme.{0}}
    (j : V ⟶ W) [IsOpenImmersion j] (p : W ⟶ Spec A) (M : ModuleCat A) :
    (pullback j).obj (E p M) ≅ E (j ≫ p) M := by
…
```
Mentions: OAI.CoherentModelActual.E

def OAI.CoherentModelActual.openPullbackEIsoOfComp line 665

Source documentation

The same comparison with a specified structural map on the chart.

def openPullbackEIsoOfComp {A : CommRingCat.{0}} {V W : Scheme.{0}}
    (j : V ⟶ W) [IsOpenImmersion j] (p : W ⟶ Spec A)
    (q : V ⟶ Spec A) (h : j ≫ p = q) (M : ModuleCat A) :
    (pullback j).obj (E p M) ≅ E q M :=
…

Mentions: OAI.CoherentModelActual.E