Uses the existing section rings and modules to represent their actual restriction maps.
The actual ring of sections at an open.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef sectionRing (X : Scheme.{u}) (U : X.Opens) : CommRingCat.{u}The actual module object, with its existing section-ring action.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef sectionModule {X : Scheme.{u}} (M : X.Modules) (U : X.Opens) :
ModuleCat.{u} (sectionRing X U)The actual abelian section-group object.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef sectionGroup {X : Scheme.{u}} (M : X.Modules) (U : X.Opens) : AddCommGrpCat.{u}The actual section-ring restriction homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef ringRestriction {X : Scheme.{u}} {U V : X.Opens} (h : V ≤ U) :
sectionRing X U →+* sectionRing X VThe actual local module viewed through the prescribed section restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef restrictedModule {X : Scheme.{u}} (M : X.Modules) {U V : X.Opens} (h : V ≤ U) :
ModuleCat.{u} (sectionRing X U)The native presheaf restriction morphism, without projecting its carrier.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef restriction {X : Scheme.{u}} (M : X.Modules) {U V : X.Opens} (h : V ≤ U) :
sectionModule M U ⟶ restrictedModule M hThe function underlying that same native restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef restrictionFn {X : Scheme.{u}} (M : X.Modules) {U V : X.Opens} (h : V ≤ U) :
sectionGroup M U → sectionGroup M VThe existing source action, exposed only as its actual power function.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef sourcePowFn {X : Scheme.{u}} (M : X.Modules) (U : X.Opens)
(f : sectionRing X U) (n : ℕ) : sectionGroup M U → sectionGroup M UThe existing restricted action, exposed only as its actual power function.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionsdef restrictedPowFn {X : Scheme.{u}} (M : X.Modules) {U V : X.Opens} (h : V ≤ U)
(f : sectionRing X U) (n : ℕ) : sectionGroup M V → sectionGroup M VLiteral computation against the original abelian restriction map.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionstheorem restrictionFn_apply {X : Scheme.{u}} (M : X.Modules) {U V : X.Opens}
(h : V ≤ U) (x : Γ(M, U)) :
restrictionFn M h x = M.presheaf.map (homOfLE h).op xLiteral computation against the original source action.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionstheorem sourcePowFn_apply {X : Scheme.{u}} (M : X.Modules) (U : X.Opens)
(f : Γ(X, U)) (n : ℕ) (x : Γ(M, U)) :
sourcePowFn M U f n x = f ^ n • xLiteral computation of the prescribed restriction-of-scalars action.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Modules.NativeSectionstheorem restrictedPowFn_apply {X : Scheme.{u}} (M : X.Modules) {U V : X.Opens}
(h : V ≤ U) (f : Γ(X, U)) (n : ℕ) (x : Γ(M, V)) :
restrictedPowFn M h f n x = X.presheaf.map (homOfLE h).op (f ^ n) • x