public import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

public import Mathlib.CategoryTheory.Category.Cat

public import Mathlib.CategoryTheory.EssentiallySmall

@[expose] public section

namespace CategoryTheory

universe w v u

variable {C : Type u} [Category.{v} C]

def Functor.Elements (F : C ⥤ Type w) :=

Σ c : C, F.obj c

abbrev Functor.elementsMk (F : C ⥤ Type w) (X : C) (x : F.obj X) : F.Elements := ⟨X, x⟩

lemma Functor.Elements.ext {F : C ⥤ Type w} (x y : F.Elements) (h₁ : x.fst = y.fst)

(h₂ : F.map (eqToHom h₁) x.snd = y.snd) : x = y := by

cases x

cases y

cases h₁

simp_all

instance categoryOfElements (F : C ⥤ Type w) : Category.{v} F.Elements where

Hom p q := { f : p.1 ⟶ q.1 // (F.map f) p.2 = q.2 }

id p := ⟨𝟙 p.1, by simp⟩

comp {X Y Z} f g := ⟨f.val ≫ g.val, by simp [f.2, g.2]⟩

def NatTrans.mapElements {F G : C ⥤ Type w} (φ : F ⟶ G) : F.Elements ⥤ G.Elements where

obj := fun ⟨X, x⟩ ↦ ⟨_, φ.app X x⟩

map {p q} := fun ⟨f, h⟩ ↦ ⟨f, by have hb := φ.naturality_apply f p.2; cat_disch⟩

def Functor.elementsFunctor : (C ⥤ Type w) ⥤ Cat where

obj F := Cat.of F.Elements

map n := (NatTrans.mapElements n).toCatHom

namespace CategoryOfElements

def homMk {F : C ⥤ Type w} (x y : F.Elements) (f : x.1 ⟶ y.1) (hf : F.map f x.snd = y.snd) :

x ⟶ y :=

⟨f, hf⟩

theorem ext (F : C ⥤ Type w) {x y : F.Elements} (f g : x ⟶ y) (w : f.val = g.val) : f = g :=

Subtype.ext w

theorem comp_val {F : C ⥤ Type w} {p q r : F.Elements} {f : p ⟶ q} {g : q ⟶ r} :

(f ≫ g).val = f.val ≫ g.val :=

rfl

theorem id_val {F : C ⥤ Type w} {p : F.Elements} : (𝟙 p : p ⟶ p).val = 𝟙 p.1 :=

rfl

theorem map_snd {F : C ⥤ Type w} {p q : F.Elements} (f : p ⟶ q) : (F.map f.val) p.2 = q.2 :=

f.property

def isoMk {F : C ⥤ Type w} (x y : F.Elements) (e : x.1 ≅ y.1)

(he : F.map e.hom x.snd = y.snd) : x ≅ y where

hom := homMk x y e.hom he

inv := homMk y x e.inv (by rw [← he, Functor.map_hom_inv'_apply])

instance [LocallySmall.{w} C] (F : C ⥤ Type w) : LocallySmall.{w} F.Elements where

hom_small := by

rintro ⟨X, _⟩ ⟨Y, y⟩

exact small_of_injective (f := fun g ↦ g.val) (by cat_disch)

end CategoryOfElements

instance groupoidOfElements {G : Type u} [Groupoid.{v} G] (F : G ⥤ Type w) :

Groupoid F.Elements where

inv {p q} f :=

⟨Groupoid.inv f.val,

calc

F.map (Groupoid.inv f.val) q.2 = F.map (Groupoid.inv f.val) (F.map f.val p.2) := by rw [f.2]

_ = (F.map f.val ≫ F.map (Groupoid.inv f.val)) p.2 := rfl

_ = p.2 := by

rw [← F.map_comp]

simp

⟩

inv_comp _ := by

ext

simp

comp_inv _ := by

ext

simp

namespace CategoryOfElements

variable (F : C ⥤ Type w)

def π : F.Elements ⥤ C where

obj X := X.1

map f := f.val

instance : (π F).Faithful where

instance : (π F).ReflectsIsomorphisms where

reflects f h := by

refine ⟨⟨(inv ((π F).map f) :), ?_⟩, ?_, ?_⟩

· simp only [← map_snd f, ← Functor.map_comp_apply,

π_obj, π_map, IsIso.hom_inv_id, Functor.map_id_apply]

· cat_disch

· cat_disch

def map {F₁ F₂ : C ⥤ Type w} (α : F₁ ⟶ F₂) : F₁.Elements ⥤ F₂.Elements where

obj t := ⟨t.1, α.app t.1 t.2⟩

map {t₁ t₂} k := ⟨k.1, by simpa [map_snd] using (NatTrans.naturality_apply α k.1 t₁.2).symm⟩

theorem map_π {F₁ F₂ : C ⥤ Type w} (α : F₁ ⟶ F₂) : map α ⋙ π F₂ = π F₁ :=

rfl

def toStructuredArrow : F.Elements ⥤ StructuredArrow PUnit F where

obj X := StructuredArrow.mk <| ↾fun _ => X.2

map {X Y} f := StructuredArrow.homMk f.val (by ext; simp [f.2])

theorem toStructuredArrow_obj (X) :

(toStructuredArrow F).obj X =

{ left := ⟨⟨⟩⟩

right := X.1

hom := ↾fun _ => X.2 } :=

rfl

theorem to_comma_map_right {X Y} (f : X ⟶ Y) : ((toStructuredArrow F).map f).right = f.val :=

rfl

def fromStructuredArrow : StructuredArrow PUnit F ⥤ F.Elements where

obj X := Functor.elementsMk _ X.right (X.hom .unit)

map f := ⟨f.right, by simp [ConcreteCategory.congr_hom f.w.symm .unit]; rfl⟩

theorem fromStructuredArrow_obj (X) : (fromStructuredArrow F).obj X = ⟨X.right, X.hom PUnit.unit⟩ :=

rfl

theorem fromStructuredArrow_map {X Y} (f : X ⟶ Y) :

(fromStructuredArrow F).map f =

⟨f.right, by simp [ConcreteCategory.congr_hom f.w.symm PUnit.unit]; rfl⟩ :=

rfl

def structuredArrowEquivalence : F.Elements ≌ StructuredArrow PUnit F where

functor := toStructuredArrow F

inverse := fromStructuredArrow F

unitIso := Iso.refl _

counitIso := Iso.refl _

open Opposite

def toCostructuredArrow (F : Cᵒᵖ ⥤ Type v) : F.Elementsᵒᵖ ⥤ CostructuredArrow yoneda F where

obj X := CostructuredArrow.mk (yonedaEquiv.symm (unop X).2)

map f :=

CostructuredArrow.homMk f.unop.val.unop (by

ext Z y

simp [yonedaEquiv])

def fromCostructuredArrow (F : Cᵒᵖ ⥤ Type v) :

(CostructuredArrow yoneda F)ᵒᵖ ⥤ F.Elements where

obj X := ⟨op (unop X).1, yonedaEquiv.1 (unop X).3⟩

map {X Y} f := ⟨f.unop.1.op, by simp [yonedaEquiv_naturality]⟩

theorem fromCostructuredArrow_obj_mk (F : Cᵒᵖ ⥤ Type v) {X : C} (f : yoneda.obj X ⟶ F) :

(fromCostructuredArrow F).obj (op (CostructuredArrow.mk f)) = ⟨op X, yonedaEquiv.1 f⟩ :=

rfl

def costructuredArrowYonedaEquivalence (F : Cᵒᵖ ⥤ Type v) :

F.Elementsᵒᵖ ≌ CostructuredArrow yoneda F where

functor := toCostructuredArrow F

inverse := (fromCostructuredArrow F).rightOp

unitIso :=

NatIso.ofComponents

(fun X ↦ Iso.op (CategoryOfElements.isoMk _ _ (Iso.refl _) (by simp; rfl))) (by

rintro ⟨x⟩ ⟨y⟩ ⟨f : y ⟶ x⟩

exact Quiver.Hom.unop_inj (by ext; simp))

counitIso := NatIso.ofComponents (fun X ↦ CostructuredArrow.isoMk (Iso.refl _) (by

dsimp

simpa only [Functor.map_id, Category.id_comp] using

(yonedaEquiv.symm_apply_apply X.hom).symm))

theorem costructuredArrow_yoneda_equivalence_naturality {F₁ F₂ : Cᵒᵖ ⥤ Type v} (α : F₁ ⟶ F₂) :

(map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α := by

fapply Functor.ext

· intro X

simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,

Functor.comp_obj]

congr

ext _ f

exact (α.naturality_apply f.op (unop X).snd).symm

· simp

def costructuredArrowYonedaEquivalenceFunctorProj (F : Cᵒᵖ ⥤ Type v) :

(costructuredArrowYonedaEquivalence F).functor ⋙ CostructuredArrow.proj _ _ ≅ (π F).leftOp :=

Iso.refl _

def costructuredArrowYonedaEquivalenceInverseπ (F : Cᵒᵖ ⥤ Type v) :

(costructuredArrowYonedaEquivalence F).inverse ⋙ (π F).leftOp ≅ CostructuredArrow.proj _ _ :=

Iso.refl _

set_option backward.isDefEq.respectTransparency false in

def costructuredArrowULiftYonedaEquivalence (F : Cᵒᵖ ⥤ Type (max w v)) :

F.Elementsᵒᵖ ≌ CostructuredArrow uliftYoneda.{w} F where

functor :=

{ obj x := CostructuredArrow.mk (uliftYonedaEquiv.{w}.symm x.unop.2)

map f := CostructuredArrow.homMk f.1.1.unop (by

dsimp

rw [← uliftYonedaEquiv_symm_map, map_snd]) }

inverse :=

{ obj X := op (F.elementsMk _ (uliftYonedaEquiv.{w} X.hom))

map f := (homMk _ _ f.left.op (by

dsimp

rw [← CostructuredArrow.w f, uliftYonedaEquiv_naturality, Quiver.Hom.unop_op])).op }

unitIso := NatIso.ofComponents (fun x ↦ Iso.op (isoMk _ _ (Iso.refl _) (by

dsimp

simpa only [Functor.map_id_apply] using

uliftYonedaEquiv.apply_symm_apply (unop x).snd)))

(fun f ↦ Quiver.Hom.unop_inj (by aesop))

counitIso := NatIso.ofComponents (fun X ↦ CostructuredArrow.isoMk (Iso.refl _))

def costructuredArrowULiftYonedaEquivalenceFunctorCompProjIso (F : Cᵒᵖ ⥤ Type (max w v)) :

(costructuredArrowULiftYonedaEquivalence.{w} F).functor ⋙ CostructuredArrow.proj _ _ ≅

(π F).leftOp :=

Iso.refl _

end CategoryOfElements

namespace Functor

def Elements.initialOfRepresentableBy {F : Cᵒᵖ ⥤ Type*} {X : C} (h : F.RepresentableBy X) :

F.Elements :=

⟨.op X, h.homEquiv (𝟙 X)⟩

set_option backward.isDefEq.respectTransparency false in

def Elements.isInitialOfRepresentableBy {F : Cᵒᵖ ⥤ Type*} {X : C} (h : F.RepresentableBy X) :

Limits.IsInitial (initialOfRepresentableBy h) :=

.ofUniqueHom (fun Y ↦ ⟨h.homEquiv.symm Y.snd |>.op, by simp [← h.homEquiv_comp]⟩) fun Y m ↦ by

simp [← m.2, ← h.homEquiv_unop_comp]

def Elements.initialOfCorepresentableBy {F : C ⥤ Type*} {X : C} (h : F.CorepresentableBy X) :

F.Elements :=

⟨X, h.homEquiv (𝟙 X)⟩

set_option backward.isDefEq.respectTransparency false in

def Elements.isInitialOfCorepresentableBy {F : C ⥤ Type*} {X : C} (h : F.CorepresentableBy X) :

Limits.IsInitial (initialOfCorepresentableBy h) :=

.ofUniqueHom (fun Y ↦ ⟨h.homEquiv.symm Y.snd, by simp [← h.homEquiv_comp]⟩) fun Y m ↦ by

simp [← m.2, ← h.homEquiv_comp]

def Elements.initial (A : C) : (yoneda.obj A).Elements :=

⟨Opposite.op A, 𝟙 _⟩

def Elements.isInitial (A : C) : Limits.IsInitial (Elements.initial A) :=

isInitialOfRepresentableBy (.yoneda A)

end Functor

end CategoryTheory