ModuleNativeSectionObjects.lean
Nyll.SchemeTheory.Modules.NativeSectionObjects
4 declarations indexed from sourceView source ↗ Module documentation
Native section objects for pushforward comparison
Keeps section opens, rings and modules in their existing categorical objects.
Imports4
- Mathlib.AlgebraicGeometry.Scheme
- Mathlib.AlgebraicGeometry.Modules.Sheaf
- Mathlib.Algebra.Category.ModuleCat.Basic
- Mathlib.Algebra.Category.Grp.Basic
Imported by3
Declarations
AlgebraicGeometry.Scheme.Hom.sectionComparisonOpen
DocumentationThe actual preimage open, computed before evaluating any module.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom
AlgebraicGeometry.Scheme.Hom.sectionComparisonRing
DocumentationThe existing commutative section-ring object on that open.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom
AlgebraicGeometry.Scheme.Hom.sectionComparisonModule
DocumentationThe existing native section module; no module action is installed or reconstructed.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom
AlgebraicGeometry.Scheme.Hom.sectionComparisonGroup
DocumentationThe existing underlying abelian section-group object at the computed open.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom