Concrete sites

Concrete sites are concrete categories whose forgetful functor is corepresented by a terminal object, equipped with a Grothendieck topology consisting only of jointly surjective sieves. See https://ncatlab.org/nlab/show/concrete+site.

Also see https://arxiv.org/abs/0807.1704; note that while that article requires concrete sites to be subcanonical, we don't require that here.

Main definitions / results:

• Presieve.IsJointlySurjective: property stating that a presieve in a concrete category is jointly surjective
• IsConcreteSite: typeclass giving a site the structure of a concrete site
• IsConcreteSite.isLocalSite: every concrete site is also a local site
• IsConcreteSite.isSeparated_of_isRepresentable: every representable presheaf on a concrete site is separated. In particular, to show that a concrete site is subcanonical it suffices to show the existence part of the sheaf condition for representable sheaves.

There is also some material on concrete sheaves, but they should probably be redefined in terms of local sites / biseparated sheaves before being expanded upon.

TODOs

• maybe split out concrete categories where points correspond to morphisms from a terminal object into a separate definition / file

def CategoryTheory.Presieve.IsJointlySurjective {C : Type u} [Category.{v, u} C] {FC : C → C → Type w} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X : C} (S : Presieve X) : Prop

A presieve S on X in a concrete category is jointly surjective if every x : X is in the image of some f in S.

Equations

• S.IsJointlySurjective = ∀ (x : CategoryTheory.ToType X), ∃ (Y : C) (f : Y ⟶ X), S f ∧ ∃ (y : CC Y), (CategoryTheory.ConcreteCategory.hom f) y = x

theorem CategoryTheory.Presieve.isJointlySurjective_iff_iUnion_range_eq_univ {C : Type u} [Category.{v, u} C] {FC : C → C → Type w} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X : C} {S : Presieve X} : S.IsJointlySurjective ↔ ⋃ (Y : C), ⋃ (f : Y ⟶ X), ⋃ (_ : S f), Set.range ⇑(ConcreteCategory.hom f) = Set.univ

theorem CategoryTheory.Presieve.IsJointlySurjective.iUnion_eq_univ {C : Type u} [Category.{v, u} C] {FC : C → C → Type w} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X : C} {S : Presieve X} (hS : S.IsJointlySurjective) : ⋃ (Y : C), ⋃ (f : Y ⟶ X), ⋃ (_ : S f), Set.range ⇑(ConcreteCategory.hom f) = Set.univ

theorem CategoryTheory.Presieve.IsJointlySurjective.mono {C : Type u} [Category.{v, u} C] {FC : C → C → Type w} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {X : C} {S R : Presieve X} (hR : S ≤ R) (hS : S.IsJointlySurjective) : R.IsJointlySurjective

class CategoryTheory.GrothendieckTopology.IsConcreteSite {C : Type u} [Category.{v, u} C] (FC : outParam (C → C → Type v)) {CC : outParam (C → Type v)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] (J : GrothendieckTopology C) extends CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) C, CategoryTheory.ConcreteCategory C FC : Type (max u v)

A site is concrete if it is a concrete category in such a way that points correspond to morphisms from a terminal object, and all sieves are jointly surjective.

• has_limit (F : Functor (Discrete PEmpty.{1}) C) : HasLimit F
• hom {X Y : C} : (X ⟶ Y) → FC X Y
• ofHom {X Y : C} : FC X Y → (X ⟶ Y)
• hom_ofHom {X Y : C} (f : FC X Y) : hom (ofHom f) = f
• ofHom_hom {X Y : C} (f : X ⟶ Y) : ofHom (hom f) = f
• id_apply {X : C} (x : CC X) : (hom (CategoryStruct.id X)) x = x
• comp_apply {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : CC X) : (hom (CategoryStruct.comp f g)) x = (hom g) ((hom f) x)
• forgetNatIsoCoyoneda : forget C ≅ coyoneda.obj (Opposite.op (⊤_ C))

  The forgetful functor is given by morphisms from the terminal object. Since a forgetful functor might already exists, this is encoded here as a natural isomorphism.

• forgetNatIsoCoyoneda_apply {X : C} {x : ToType X} : ⇑(ConcreteCategory.hom (forgetNatIsoCoyoneda.hom.app X x)) = fun (x_1 : CC (Opposite.unop (Opposite.op (⊤_ C)))) => x

  Said isomorphism takes x : X to a morphism with underlying map fun _ ↦ x.

• isJointlySurjective_of_mem {X : C} {S : Sieve X} (hS : S ∈ J X) : S.arrows.IsJointlySurjective

  All covering sieves are jointly surjective.

theorem CategoryTheory.GrothendieckTopology.IsConcreteSite.coyoneda_obj_terminal_faithful {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [IsConcreteSite FC J] : (coyoneda.obj (Opposite.op (⊤_ C))).Faithful

@[implicit_reducible]

noncomputable instance CategoryTheory.GrothendieckTopology.IsConcreteSite.instUniqueTerminal {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [IsConcreteSite FC J] : Unique (ToType (⊤_ C))

The terminal object of a concrete site has exactly one point.

Equations

• CategoryTheory.GrothendieckTopology.IsConcreteSite.instUniqueTerminal J = (CategoryTheory.GrothendieckTopology.IsConcreteSite.forgetNatIsoCoyoneda.app (⊤_ C)).toEquiv.unique

instance CategoryTheory.GrothendieckTopology.IsConcreteSite.isLocalSite {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [IsConcreteSite FC J] : J.IsLocalSite

Every concrete site is also a local site.

theorem CategoryTheory.GrothendieckTopology.IsConcreteSite.from_terminal_mem_of_mem {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [IsConcreteSite FC J] {X : C} {S : Sieve X} (hS : S ∈ J X) (f : ⊤_ C ⟶ X) : S.arrows f

On concrete sites, covering sieves contain all morphisms from the terminal object.

theorem CategoryTheory.GrothendieckTopology.IsConcreteSite.isSeparated_yoneda_obj {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [IsConcreteSite FC J] (X : C) : Presieve.IsSeparated J (yoneda.obj X)

theorem CategoryTheory.GrothendieckTopology.IsConcreteSite.isSeparated_of_isRepresentable {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [IsConcreteSite FC J] (F : Functor Cᵒᵖ (Type v)) [F.IsRepresentable] : Presieve.IsSeparated J F

Every representable presheaf on a concrete site is, while not necessarily a sheaf, at least separated.

def CategoryTheory.Presheaf.IsConcrete {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [GrothendieckTopology.IsConcreteSite FC J] (P : Functor Cᵒᵖ (Type w)) : Prop

Equations

• CategoryTheory.Presheaf.IsConcrete J P = ∀ (X : C), Function.Injective fun (p : P.obj (Opposite.op X)) (f : ⊤_ C ⟶ X) => P.map f.op p

structure CategoryTheory.ConcreteSheaf {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [GrothendieckTopology.IsConcreteSite FC J] extends CategoryTheory.ObjectProperty.FullSubcategory (CategoryTheory.Presheaf.IsSheaf J) : Type (max (max u v) (w + 1))

The category of concrete sheaves.

• obj : Functor Cᵒᵖ (Type w)
• property : Presheaf.IsSheaf J self.obj
• concrete : Presheaf.IsConcrete J self.obj

@[reducible, inline]

abbrev CategoryTheory.ConcreteSheaf.toSheaf {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] {J : GrothendieckTopology C} [GrothendieckTopology.IsConcreteSite FC J] (P : ConcreteSheaf J) : Sheaf J (Type w)

Equations

• P.toSheaf = P.toFullSubcategory

@[implicit_reducible]

instance CategoryTheory.instCategoryConcreteSheaf {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [GrothendieckTopology.IsConcreteSite FC J] : Category.{max u u_1, max (max (u_1 + 1) v) u} (ConcreteSheaf J)

Morphisms of concrete sheaves are simply morphisms of sheaves.

Equations

• CategoryTheory.instCategoryConcreteSheaf J = CategoryTheory.InducedCategory.instCategory

def CategoryTheory.concreteSheafToSheaf {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [GrothendieckTopology.IsConcreteSite FC J] : Functor (ConcreteSheaf J) (Sheaf J (Type w))

The forgetful functor from concrete sheaves to sheaves.

Equations

• CategoryTheory.concreteSheafToSheaf J = CategoryTheory.inducedFunctor CategoryTheory.ConcreteSheaf.toFullSubcategory

def CategoryTheory.fullyFaithfulConcreteSheafToSheaf {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [GrothendieckTopology.IsConcreteSite FC J] : (concreteSheafToSheaf J).FullyFaithful

Equations

• CategoryTheory.fullyFaithfulConcreteSheafToSheaf J = CategoryTheory.fullyFaithfulInducedFunctor CategoryTheory.ConcreteSheaf.toFullSubcategory

instance CategoryTheory.instFullConcreteSheafSheafTypeConcreteSheafToSheaf {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [GrothendieckTopology.IsConcreteSite FC J] : (concreteSheafToSheaf J).Full

instance CategoryTheory.instFaithfulConcreteSheafSheafTypeConcreteSheafToSheaf {C : Type u} [Category.{v, u} C] {FC : C → C → Type v} {CC : C → Type v} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] (J : GrothendieckTopology C) [GrothendieckTopology.IsConcreteSite FC J] : (concreteSheafToSheaf J).Faithful