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

• switch from HasForget to the new ConcreteCategory API
• 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] [HasForget C] {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.forget C).obj X), ∃ (Y : C), ∃ f ∈ S, ∃ (y : (CategoryTheory.forget C).obj Y), f y = x

theorem CategoryTheory.Presieve.isJointlySurjective_iff_iUnion_range_eq_univ {C : Type u} [Category.{v, u} C] [HasForget C] {X : C} {S : Presieve X} : S.IsJointlySurjective ↔ ⋃ (Y : C), ⋃ f ∈ S, Set.range ⇑f = Set.univ

theorem CategoryTheory.Presieve.IsJointlySurjective.iUnion_eq_univ {C : Type u} [Category.{v, u} C] [HasForget C] {X : C} {S : Presieve X} (hS : S.IsJointlySurjective) : ⋃ (Y : C), ⋃ f ∈ S, Set.range ⇑f = Set.univ

theorem CategoryTheory.Presieve.IsJointlySurjective.mono {C : Type u} [Category.{v, u} C] [HasForget C] {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] (J : GrothendieckTopology C) extends CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) C, CategoryTheory.HasForget C : Type (max u (v + 1))

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
• forget : Functor C (Type v)
• forget_faithful : HasForget.forget.Faithful
• 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 : (forget C).obj X} : ⇑(forgetNatIsoCoyoneda.hom.app X x) = fun (x_1 : (forget C).obj (⊤_ 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] (J : GrothendieckTopology C) [J.IsConcreteSite] : (coyoneda.obj (Opposite.op (⊤_ C))).Faithful

noncomputable instance CategoryTheory.GrothendieckTopology.IsConcreteSite.instUniqueTerminal {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsConcreteSite] : Unique ((forget C).obj (⊤_ 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] (J : GrothendieckTopology C) [J.IsConcreteSite] : 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] (J : GrothendieckTopology C) [J.IsConcreteSite] {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] (J : GrothendieckTopology C) [J.IsConcreteSite] (X : C) : Presieve.IsSeparated J (yoneda.obj X)

theorem CategoryTheory.Presieve.isSeparatedFor_iso {C : Type u} [Category.{v, u} C] {F F' : Functor Cᵒᵖ (Type w)} (i : F ≅ F') {X : C} {R : Presieve X} (hF : IsSeparatedFor F R) : IsSeparatedFor F' R

The property of being separated for some presieve is preserved under isomorphisms. TODO: upstream to mathlib.

theorem CategoryTheory.Presieve.isSeparated_iso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {F F' : Functor Cᵒᵖ (Type w)} (i : F ≅ F') (hF : IsSeparated J F) : IsSeparated J F'

The property of being separated is preserved under isomorphisms. TODO: upstream to mathlib.

theorem CategoryTheory.GrothendieckTopology.IsConcreteSite.isSeparated_of_isRepresentable {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsConcreteSite] (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] (J : GrothendieckTopology C) [J.IsConcreteSite] (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] (J : GrothendieckTopology C) [J.IsConcreteSite] extends CategoryTheory.Sheaf J (Type w) : Type (max (max u v) (w + 1))

The category of concrete sheaves.

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

instance CategoryTheory.instCategoryConcreteSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsConcreteSite] : 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.category CategoryTheory.ConcreteSheaf.toSheaf

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

The forgetful functor from concrete sheaves to sheaves.

Equations

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

def CategoryTheory.fullyFaithfulConcreteSheafToSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsConcreteSite] : (concreteSheafToSheaf J).FullyFaithful

Equations

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

instance CategoryTheory.instFullConcreteSheafSheafTypeConcreteSheafToSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsConcreteSite] : (concreteSheafToSheaf J).Full

instance CategoryTheory.instFaithfulConcreteSheafSheafTypeConcreteSheafToSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) [J.IsConcreteSite] : (concreteSheafToSheaf J).Faithful