Quotient presentations of module sheaves

This file defines the elementary input to a Quot construction: an actual epimorphism from a fixed module sheaf. Morphisms are maps of targets commuting with the quotient arrows. Pullback of module sheaves preserves these presentations because it preserves finite colimits, so quotient presentations have a genuine base-change operation before any representability theorem is claimed.

No scheme named QuotScheme is introduced here. Representability, when it is available, is a separate Yoneda universal property.

structure AlgebraicGeometry.ModuleQuotient {X : Scheme} (F : X.Modules) : Type (u + 1)

An epimorphic presentation F ⟶ Q of a quotient module sheaf.

• target : X.Modules

  The quotient module sheaf.

• hom : F ⟶ self.target

  The quotient arrow.

• isEpi : CategoryTheory.Epi self.hom

  The quotient arrow is an epimorphism.

instance AlgebraicGeometry.ModuleQuotient.hom_isEpi {X : Scheme} {F : X.Modules} (q : ModuleQuotient F) : CategoryTheory.Epi q.hom

structure AlgebraicGeometry.ModuleQuotient.Hom {X : Scheme} {F : X.Modules} (q r : ModuleQuotient F) : Type u

A morphism of quotient presentations is a commuting map of targets.

• right : q.target ⟶ r.target

  The map between quotient targets.

• comm : CategoryTheory.CategoryStruct.comp q.hom self.right = r.hom

  Compatibility with the two quotient arrows.

theorem AlgebraicGeometry.ModuleQuotient.Hom.ext {X : Scheme} {F : X.Modules} {q r : ModuleQuotient F} (f g : q.Hom r) (h : f.right = g.right) : f = g

theorem AlgebraicGeometry.ModuleQuotient.Hom.ext_iff {X : Scheme} {F : X.Modules} {q r : ModuleQuotient F} {f g : q.Hom r} : f = g ↔ f.right = g.right

@[implicit_reducible]

instance AlgebraicGeometry.ModuleQuotient.category {X : Scheme} {F : X.Modules} : CategoryTheory.Category.{u, u + 1} (ModuleQuotient F)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.ModuleQuotient.id_right {X : Scheme} {F : X.Modules} (q : ModuleQuotient F) : (CategoryTheory.CategoryStruct.id q).right = CategoryTheory.CategoryStruct.id q.target

@[simp]

theorem AlgebraicGeometry.ModuleQuotient.comp_right {X : Scheme} {F : X.Modules} {q r s : ModuleQuotient F} (f : q ⟶ r) (g : r ⟶ s) : (CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right

def AlgebraicGeometry.ModuleQuotient.targetFunctor {X : Scheme} (F : X.Modules) : CategoryTheory.Functor (ModuleQuotient F) X.Modules

The forgetful functor from quotient presentations to their targets.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.ModuleQuotient.pullback {X Y : Scheme} (f : X ⟶ Y) {G : Y.Modules} (q : ModuleQuotient G) : ModuleQuotient ((Scheme.Modules.pullback f).obj G)

Pull a quotient presentation back along a scheme morphism.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.ModuleQuotient.pullbackFunctor {X Y : Scheme} (f : X ⟶ Y) (G : Y.Modules) : CategoryTheory.Functor (ModuleQuotient G) (ModuleQuotient ((Scheme.Modules.pullback f).obj G))

Pullback acts functorially on the categories of quotient presentations.

Equations

• One or more equations did not get rendered due to their size.

def AlgebraicGeometry.ModuleQuotient.identity {X : Scheme} (F : X.Modules) : ModuleQuotient F

The identity arrow presents a module sheaf as a quotient of itself.

Equations

• AlgebraicGeometry.ModuleQuotient.identity F = { target := F, hom := CategoryTheory.CategoryStruct.id F, isEpi := ⋯ }

noncomputable def AlgebraicGeometry.ModuleQuotient.zero (X : Scheme) : ModuleQuotient 0

The zero module sheaf has its canonical identity quotient.

Equations

• AlgebraicGeometry.ModuleQuotient.zero X = AlgebraicGeometry.ModuleQuotient.identity 0

noncomputable def AlgebraicGeometry.ModuleQuotient.pullbackIdentityIso {X Y : Scheme} (f : X ⟶ Y) (G : Y.Modules) : pullback f (identity G) ≅ identity ((Scheme.Modules.pullback f).obj G)

Pullback of the identity quotient is canonically isomorphic to the identity quotient of the pulled-back module.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.ModuleQuotient.pullbackZeroIso {X Y : Scheme} (f : X ⟶ Y) : pullback f (zero Y) ≅ identity ((Scheme.Modules.pullback f).obj 0)

In particular, the zero quotient is preserved by every scheme base change, up to the canonical pullback comparison for zero module sheaves.

Equations

• AlgebraicGeometry.ModuleQuotient.pullbackZeroIso f = AlgebraicGeometry.ModuleQuotient.pullbackIdentityIso f 0