Module

PullbackRepresentable.lean

Nyll.SchemeTheory.FiniteEtale.PullbackRepresentable

1 declaration indexed from sourceView source ↗

Module documentation

Recovering a representer after pullback along a monomorphism

Postcomposition with a monomorphism is fully faithful on slice categories. The unit of its pullback adjunction is therefore invertible. Restricting a representation of T ↦ Hom(i⁎ T, V) to the smaller slice recovers V by uniqueness of representing objects.

Imports4

Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.CategoryTheory.Adjunction.FullyFaithful
Mathlib.CategoryTheory.Comma.Over.Pullback
Mathlib.CategoryTheory.Yoneda

Imported by2

def

pullbackIsoOfRepresentable

L34 ↗

AlgebraicGeometry.FiniteEtale.pullbackIsoOfRepresentable

Documentation

If the presheaf obtained by precomposing Hom(-, V) with pullback along a monomorphism is represented by W, then pulling W back gives V. No finiteness, étaleness, or surjectivity hypothesis is needed.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public noncomputable section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

def pullbackIsoOfRepresentable {X Y : Scheme.{u}} (i : X ⟶ Y) [Mono i]
    (V : Over X) (W : Over Y)
    (h : ((Over.pullback i).op ⋙ yoneda.obj V).RepresentableBy W) :
    (Over.pullback i).obj W ≅ V

Module documentation

Recovering a representer after pullback along a monomorphism

Declarations

pullbackIsoOfRepresentable