ModuleFiniteTypeQuotient.lean
Nyll.SchemeTheory.Modules.FiniteTypeQuotient
2 declarations indexed from sourceView source ↗ Module documentation
Finite type passes to actual epimorphic quotients
The original local generating covers are retained. Restriction to a slice is a left adjoint, so the actual restricted morphisms are epimorphisms; their images of the original finite generators generate the quotient.
Imports4
- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
- Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian
- Mathlib.CategoryTheory.Adjunction.Limits
- Mathlib.CategoryTheory.Functor.EpiMono
Imported by3
Declarations
SheafOfModules.isFiniteType_of_epi
DocumentationAn epimorphic quotient of a finite-type sheaf of modules is finite type.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] [HasBinaryProducts C]
{J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
[∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
[∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
SheafOfModules.isFiniteType_of_iso
DocumentationFinite type is transported along an actual isomorphism.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u} [Category.{v} C] [HasBinaryProducts C]
{J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
[∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
[∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]