Cohesive categories

A topos C is called cohesive over another topos D (typically Type) if it is equipped with a quadruple π₀ ⊣ disc ⊣ Γ ⊣ codisc of adjoint functors between them, the first of which preserves finite products, and the second and fourth of which are fully faithful. We formalise this here by defining a typeclass CohesiveStructure C D carrying such a quadruple between arbitrary categories C and D, since mathlib does not much on topoi yet.

See https://ncatlab.org/nlab/show/cohesive+topos for cohesive topoi, and also the paper "Axiomatic Cohesion" by Lawvere for more general cohesive categories.

class CategoryTheory.CohesiveStructure (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] : Type (max (max (max u u') v) v')

Typeclass equipping a category with the adjoint quadruple of functors that is also used to define e.g. cohesive topoi. Since topoi are not in mathlib yet I am stating this for general categories, but it should probably be changed to something more specific like cohesive topoi or "categories of cohesion" in the sense of Lawvere.

• π₀ : Functor C D
• disc : Functor D C
• Γ : Functor C D
• codisc : Functor D C
• π₀DiscAdj : π₀ ⊣ disc
• discΓAdj : disc ⊣ Γ
• ΓCodiscAdj : Γ ⊣ codisc
• preservesFiniteProducts_π₀ : Limits.PreservesFiniteProducts π₀
• fullyFaithfulDisc : disc.FullyFaithful
• fullyFaithfulCodisc : codisc.FullyFaithful

instance CategoryTheory.Cohesive.instIsLeftAdjointπ₀ (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : π₀.IsLeftAdjoint

instance CategoryTheory.Cohesive.instIsRightAdjointDisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : disc.IsRightAdjoint

instance CategoryTheory.Cohesive.instIsLeftAdjointDisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : disc.IsLeftAdjoint

instance CategoryTheory.Cohesive.instIsRightAdjointΓ (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Γ.IsRightAdjoint

instance CategoryTheory.Cohesive.instIsLeftAdjointΓ (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Γ.IsLeftAdjoint

instance CategoryTheory.Cohesive.instIsRightAdjointCodisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : codisc.IsRightAdjoint

instance CategoryTheory.Cohesive.instPreservesFiniteProductsπ₀ (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Limits.PreservesFiniteProducts π₀

instance CategoryTheory.Cohesive.instFullDisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : disc.Full

instance CategoryTheory.Cohesive.instFaithfulDisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : disc.Faithful

instance CategoryTheory.Cohesive.instFullCodisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : codisc.Full

instance CategoryTheory.Cohesive.instFaithfulCodisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : codisc.Faithful

def CategoryTheory.Cohesive.shape (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Monad C

The shape modality on a cohesive category.

Equations

• CategoryTheory.Cohesive.shape C D = CategoryTheory.CohesiveStructure.π₀DiscAdj.toMonad

@[simp]

theorem CategoryTheory.Cohesive.shape_map (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (shape C D).map f = disc.map (π₀.map f)

@[simp]

theorem CategoryTheory.Cohesive.shape_μ_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (shape C D).μ.app X = disc.map (π₀DiscAdj.counit.app (π₀.obj X))

@[simp]

theorem CategoryTheory.Cohesive.shape_obj (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (shape C D).obj X = disc.obj (π₀.obj X)

@[simp]

theorem CategoryTheory.Cohesive.shape_η (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (shape C D).η = π₀DiscAdj.unit

def CategoryTheory.Cohesive.flat (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Comonad C

The flat modality on a cohesive category.

Equations

• CategoryTheory.Cohesive.flat C D = CategoryTheory.CohesiveStructure.discΓAdj.toComonad

@[simp]

theorem CategoryTheory.Cohesive.flat_obj (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (flat C D).obj X = disc.obj (Γ.obj X)

@[simp]

theorem CategoryTheory.Cohesive.flat_ε (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (flat C D).ε = discΓAdj.counit

@[simp]

theorem CategoryTheory.Cohesive.flat_δ_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (flat C D).δ.app X = disc.map (discΓAdj.unit.app (Γ.obj X))

@[simp]

theorem CategoryTheory.Cohesive.flat_map (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (flat C D).map f = disc.map (Γ.map f)

def CategoryTheory.Cohesive.sharp (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Monad C

The sharp modality on a cohesive category.

Equations

• CategoryTheory.Cohesive.sharp C D = CategoryTheory.CohesiveStructure.ΓCodiscAdj.toMonad

@[simp]

theorem CategoryTheory.Cohesive.sharp_μ_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (sharp C D).μ.app X = codisc.map (ΓCodiscAdj.counit.app (Γ.obj X))

@[simp]

theorem CategoryTheory.Cohesive.sharp_obj (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (sharp C D).obj X = codisc.obj (Γ.obj X)

@[simp]

theorem CategoryTheory.Cohesive.sharp_map (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (sharp C D).map f = codisc.map (Γ.map f)

@[simp]

theorem CategoryTheory.Cohesive.sharp_η (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (sharp C D).η = ΓCodiscAdj.unit

def CategoryTheory.Cohesive.shapeFlatAdj (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (shape C D).toFunctor ⊣ (flat C D).toFunctor

The shape modality is adjoint to the flat modality.

Equations

• CategoryTheory.Cohesive.shapeFlatAdj C D = CategoryTheory.CohesiveStructure.π₀DiscAdj.comp CategoryTheory.CohesiveStructure.discΓAdj

@[simp]

theorem CategoryTheory.Cohesive.shapeFlatAdj_unit_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (shapeFlatAdj C D).unit.app X = CategoryStruct.comp (π₀DiscAdj.unit.app X) (disc.map (discΓAdj.unit.app (π₀.obj X)))

@[simp]

theorem CategoryTheory.Cohesive.shapeFlatAdj_counit_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (shapeFlatAdj C D).counit.app X = CategoryStruct.comp (disc.map (π₀DiscAdj.counit.app (Γ.obj X))) (discΓAdj.counit.app X)

def CategoryTheory.Cohesive.flatSharpAdj (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (flat C D).toFunctor ⊣ (sharp C D).toFunctor

The flat modality is adjoint to the sharp modality.

Equations

• CategoryTheory.Cohesive.flatSharpAdj C D = CategoryTheory.CohesiveStructure.ΓCodiscAdj.comp CategoryTheory.CohesiveStructure.discΓAdj

@[simp]

theorem CategoryTheory.Cohesive.flatSharpAdj_unit_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (flatSharpAdj C D).unit.app X = CategoryStruct.comp (ΓCodiscAdj.unit.app X) (codisc.map (discΓAdj.unit.app (Γ.obj X)))

@[simp]

theorem CategoryTheory.Cohesive.flatSharpAdj_counit_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (flatSharpAdj C D).counit.app X = CategoryStruct.comp (disc.map (ΓCodiscAdj.counit.app (Γ.obj X))) (discΓAdj.counit.app X)

instance CategoryTheory.Cohesive.instIsLeftAdjointShape (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (shape C D).IsLeftAdjoint

instance CategoryTheory.Cohesive.instIsRightAdjointFlat (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (flat C D).IsRightAdjoint

instance CategoryTheory.Cohesive.instIsLeftAdjointFlat (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (flat C D).IsLeftAdjoint

instance CategoryTheory.Cohesive.instIsRightAdjointSharp (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (sharp C D).IsRightAdjoint

noncomputable def CategoryTheory.Cohesive.pointsToPieces (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Γ ⟶ π₀

The points-to-pieces transform Γ ⟶ π₀. The other natural transformation that is also often called the points to pieces transform is the image of this under disc.

Equations

• CategoryTheory.Cohesive.pointsToPieces C D = CategoryTheory.CohesiveStructure.π₀DiscAdj.HToF CategoryTheory.CohesiveStructure.discΓAdj

@[simp]

theorem CategoryTheory.Cohesive.pointsToPieces_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (pointsToPieces C D).app X = CategoryStruct.comp (Γ.map (π₀DiscAdj.unit.app X)) (inv (discΓAdj.unit.app (π₀.obj X)))

theorem CategoryTheory.Cohesive.pointsToPieces_eq_units (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : pointsToPieces C D = CategoryStruct.comp Γ.leftUnitor.inv (CategoryStruct.comp (whiskerRight π₀DiscAdj.unit Γ) (CategoryStruct.comp (π₀.associator disc Γ).hom (CategoryStruct.comp (inv (whiskerLeft π₀ discΓAdj.unit)) π₀.rightUnitor.hom)))

Formula for pointsToPieces C D in terms of the whiskered units of the adjunctions.

theorem CategoryTheory.Cohesive.pointsToPieces_eq (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : pointsToPieces C D = CategoryStruct.comp Γ.rightUnitor.inv (CategoryStruct.comp (inv (whiskerLeft Γ π₀DiscAdj.counit)) (CategoryStruct.comp (Γ.associator disc π₀).inv (CategoryStruct.comp (whiskerRight discΓAdj.counit π₀) π₀.leftUnitor.hom)))

Formula for pointsToPieces C D in terms of the whiskered counits of the adjunctions.

def CategoryTheory.Cohesive.discPointsToPieces (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (flat C D).toFunctor ⟶ (shape C D).toFunctor

The points-to-pieces transform flat C D ⟶ shape C D in C - since flat C D and shape C D are the compositions of Γ and π₀ with disc, we add the prefix "disc" to distinguish it from the points-to-pieces transform pointsToPieces C D : Γ ⟶ π₀ in D.

Equations

• CategoryTheory.Cohesive.discPointsToPieces C D = CategoryTheory.CategoryStruct.comp (CategoryTheory.Cohesive.flat C D).ε (CategoryTheory.Cohesive.shape C D).η

@[simp]

theorem CategoryTheory.Cohesive.discPointsToPieces_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (discPointsToPieces C D).app X = CategoryStruct.comp (discΓAdj.counit.app X) (π₀DiscAdj.unit.app X)

theorem CategoryTheory.Cohesive.discΓΑdj_homEquiv_discPointsToPieces (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X : C} : (discΓAdj.homEquiv (Γ.obj X) ((shape C D).obj X)) ((discPointsToPieces C D).app X) = Γ.map (π₀DiscAdj.unit.app X)

The components of discPointsToPieces C D are discΓAdj-adjunct to the image of the unit components of shape C D under Γ.

theorem CategoryTheory.Cohesive.π₀DiscAdj_homEquiv_symm_discPointsToPieces (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X : C} : (π₀DiscAdj.homEquiv ((flat C D).obj X) (π₀.obj X)).symm ((discPointsToPieces C D).app X) = π₀.map (discΓAdj.counit.app X)

The components of discPointsToPieces C D are π₀DiscAdj-adjunct to the image of the counit components of flat C D under π₀.

theorem CategoryTheory.Cohesive.discPointsToPieces_app_eq_disc_pointsToPieces (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X : C} : (discPointsToPieces C D).app X = disc.map ((pointsToPieces C D).app X)

The points-to-pieces transform flat C D ⟶ shape C D in C is the image of the points-to-pieces transform Γ ⟶ π₀ in D under disc : D ⥤ C.

theorem CategoryTheory.Cohesive.discPointsToPieces_eq_pointsToPieces_disc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : discPointsToPieces C D = whiskerRight (pointsToPieces C D) disc

The points-to-pieces transform flat C D ⟶ shape C D in C is the image of the points-to-pieces transform Γ ⟶ π₀ in D under disc : D ⥤ C.

noncomputable def CategoryTheory.Cohesive.discToCodisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : disc ⟶ codisc

The canonical natural transformation disc ⟶ codisc.

Equations

• CategoryTheory.Cohesive.discToCodisc C D = CategoryTheory.CohesiveStructure.discΓAdj.FToH CategoryTheory.CohesiveStructure.ΓCodiscAdj

@[simp]

theorem CategoryTheory.Cohesive.discToCodisc_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : D) : (discToCodisc C D).app X = CategoryStruct.comp (ΓCodiscAdj.unit.app (disc.obj X)) (inv (codisc.map (discΓAdj.unit.app X)))

noncomputable def CategoryTheory.Cohesive.discToCodisc_eq_units (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : discToCodisc C D = CategoryStruct.comp disc.rightUnitor.inv (CategoryStruct.comp (whiskerLeft disc ΓCodiscAdj.unit) (CategoryStruct.comp (disc.associator Γ codisc).inv (CategoryStruct.comp (inv (whiskerRight discΓAdj.unit codisc)) codisc.leftUnitor.hom)))

Formula for discToCodisc C D in terms of the whiskered units of the adjunctions.

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Cohesive.discToCodisc_eq_counits (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : discToCodisc C D = CategoryStruct.comp disc.leftUnitor.inv (CategoryStruct.comp (inv (whiskerRight ΓCodiscAdj.counit disc)) (CategoryStruct.comp (codisc.associator Γ disc).hom (CategoryStruct.comp (whiskerLeft codisc discΓAdj.counit) codisc.rightUnitor.hom)))

Formula for discToCodisc C D in terms of the whiskered counits of the adjunctions.

Equations

• ⋯ = ⋯

def CategoryTheory.Cohesive.flatToSharp (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : (flat C D).toFunctor ⟶ (sharp C D).toFunctor

The canonical natural transformation flat C D ⟶ sharp C D.

Equations

• CategoryTheory.Cohesive.flatToSharp C D = CategoryTheory.CategoryStruct.comp (CategoryTheory.Cohesive.flat C D).ε (CategoryTheory.Cohesive.sharp C D).η

@[simp]

theorem CategoryTheory.Cohesive.flatToSharp_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] (X : C) : (flatToSharp C D).app X = CategoryStruct.comp (discΓAdj.counit.app X) (ΓCodiscAdj.unit.app X)

theorem CategoryTheory.Cohesive.discΓΑdj_homEquiv_flatToSharp (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X : C} : (discΓAdj.homEquiv (Γ.obj X) ((sharp C D).obj X)) ((flatToSharp C D).app X) = Γ.map (ΓCodiscAdj.unit.app X)

The components of flatToSharp C D are discΓAdj-adjunct to the image of the unit components of sharp C D under Γ.

theorem CategoryTheory.Cohesive.ΓCodiscAdj_homEquiv_symm_flatToSharp (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X : C} : (ΓCodiscAdj.homEquiv ((flat C D).obj X) (Γ.obj X)).symm ((flatToSharp C D).app X) = Γ.map (discΓAdj.counit.app X)

The components of flatToSharp C D are ΓCodiscAdj-adjunct to the image of the counit components of flat C D under Γ.

theorem CategoryTheory.Cohesive.flatToSharp_app_eq_discToCodisc_Γ (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] {X : C} : (flatToSharp C D).app X = (discToCodisc C D).app (Γ.obj X)

The components of the natural transformation flat C D ⟶ shape C D are simply the components of the discrete-to-codiscrete transform disc ⟶ codisc at Γ.

theorem CategoryTheory.Cohesive.flatToSharp_eq_Γ_discToCodisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : flatToSharp C D = whiskerLeft Γ (discToCodisc C D)

The points-to-pieces transform flat C D ⟶ shape C D in C is the image of the points-to-pieces transform Γ ⟶ π₀ in D under disc : D ⥤ C.

@[reducible, inline]

abbrev CategoryTheory.Cohesive.PiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : Prop

Cohesion of C over D is said to satisfy pieces have points if the components of the points-to-pieces transformation in D are epimorphisms.

Equations

• CategoryTheory.Cohesive.PiecesHavePoints C D = ∀ (X : C), CategoryTheory.Epi ((CategoryTheory.Cohesive.pointsToPieces C D).app X)

instance CategoryTheory.Cohesive.instEpiFunctorPointsToPiecesOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] : Epi (pointsToPieces C D)

theorem CategoryTheory.Cohesive.piecesHavePoints_iff_epi_discPointsToPieces_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : PiecesHavePoints C D ↔ ∀ (X : C), Epi ((discPointsToPieces C D).app X)

Cohesion of C over D satisfies pieces have points iff the components of the points-to-pieces transformation in C are epimorphisms.

instance CategoryTheory.Cohesive.instEpiAppDiscPointsToPiecesOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] {X : C} : Epi ((discPointsToPieces C D).app X)

instance CategoryTheory.Cohesive.instEpiFunctorDiscPointsToPiecesOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] : Epi (discPointsToPieces C D)

theorem CategoryTheory.Cohesive.piecesHavePoints_iff_epi_Γ_shape_unit (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : PiecesHavePoints C D ↔ ∀ (X : C), Epi (Γ.map ((shape C D).η.app X))

Cohesion of C over D satisfies pieces have points iff the unit components of shape C D are mapped to epimorphisms by Γ.

instance CategoryTheory.Cohesive.instEpiMapΓAppηShapeOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] {X : C} : Epi (Γ.map ((shape C D).η.app X))

instance CategoryTheory.Cohesive.instEpiFunctorWhiskerRightηShapeΓOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] : Epi (whiskerRight (shape C D).η Γ)

theorem CategoryTheory.Cohesive.piecesHavePoints_iff_mono_discToCodisc_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : PiecesHavePoints C D ↔ ∀ (X : D), Mono ((discToCodisc C D).app X)

Cohesion of C over D satisfies pieces have points iff the components of the discrete-to-codiscrete transformation are monomorphisms.

instance CategoryTheory.Cohesive.instMonoAppDiscToCodiscOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] {X : D} : Mono ((discToCodisc C D).app X)

instance CategoryTheory.Cohesive.instMonoFunctorDiscToCodiscOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] : Mono (discToCodisc C D)

theorem CategoryTheory.Cohesive.piecesHavePoints_iff_mono_flatToSharp_app (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : PiecesHavePoints C D ↔ ∀ (X : C), Mono ((flatToSharp C D).app X)

Cohesion of C over D satisfies pieces have points iff the components of the flat-to-sharp transformation are monomorphisms.

instance CategoryTheory.Cohesive.instMonoAppFlatToSharpOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] {X : C} : Mono ((flatToSharp C D).app X)

instance CategoryTheory.Cohesive.instMonoFunctorFlatToSharpOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] : Mono (flatToSharp C D)

theorem CategoryTheory.Cohesive.piecesHavePoints_iff_mono_sharp_unit_disc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] : PiecesHavePoints C D ↔ ∀ (X : D), Mono ((sharp C D).η.app (disc.obj X))

Cohesion of C over D satisfies pieces have points iff the unit components of sharp C D on discrete objects are monomorphisms.

instance CategoryTheory.Cohesive.instMonoAppηSharpObjDisc (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] {X : D} : Mono ((sharp C D).η.app (disc.obj X))

instance CategoryTheory.Cohesive.instMonoFunctorWhiskerLeftDiscηSharpOfPiecesHavePoints (C : Type u) [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [CohesiveStructure C D] [PiecesHavePoints C D] : Mono (whiskerLeft disc (sharp C D).η)