Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
feat(category_theory): over and under categories (#549)
  • Loading branch information
jcommelin authored and johoelzl committed Jan 11, 2019
1 parent c19b4be commit 5c323cd
Show file tree
Hide file tree
Showing 2 changed files with 287 additions and 1 deletion.
134 changes: 133 additions & 1 deletion category_theory/comma.lean
Expand Up @@ -6,6 +6,8 @@ import category_theory.types
import category_theory.isomorphism
import category_theory.whiskering
import category_theory.opposites
import category_theory.punit
import category_theory.equivalence

namespace category_theory

Expand Down Expand Up @@ -152,7 +154,7 @@ section
variables {X Y : comma L R₁} {f : X ⟶ Y} {r : R₁ ⟹ R₂}
@[simp] lemma map_right_obj_left : ((map_right L r).obj X).left = X.left := rfl
@[simp] lemma map_right_obj_right : ((map_right L r).obj X).right = X.right := rfl
@[simp] lemma map_right_obj_hom : ((map_right L r).obj X).hom = X.hom ≫ r.app X.right := rfl
@[simp] lemma map_right_obj_hom : ((map_right L r).obj X).hom = X.hom ≫ r.app X.right := rfl
@[simp] lemma map_right_map_left : ((map_right L r).map f).left = f.left := rfl
@[simp] lemma map_right_map_right : ((map_right L r).map f).right = f.right := rfl
end
Expand Down Expand Up @@ -189,4 +191,134 @@ end

end comma

omit 𝒜 ℬ

def over (X : T) := comma.{v₃ 0 v₃} (functor.id T) (functor.of.obj X)

namespace over

variables {X : T}

instance category : category (over X) := by delta over; apply_instance

@[extensionality] lemma over_morphism.ext {X : T} {U V : over X} {f g : U ⟶ V}
(h : f.left = g.left) : f = g :=
by tidy

@[simp] lemma over_right (U : over X) : U.right = punit.star := by tidy
@[simp] lemma over_morphism_right {U V : over X} (f : U ⟶ V) : f.right = 𝟙 punit.star := by tidy

@[simp] lemma id_left (U : over X) : comma_morphism.left (𝟙 U) = 𝟙 U.left := rfl
@[simp] lemma comp_left (a b c : over X) (f : a ⟶ b) (g : b ⟶ c) :
(f ≫ g).left = f.left ≫ g.left := rfl

@[simp] lemma w {A B : over X} (f : A ⟶ B) : f.left ≫ B.hom = A.hom :=
by have := f.w; tidy

def mk {X Y : T} (f : Y ⟶ X) : over X :=
{ left := Y, hom := f }

@[simp] lemma mk_left {X Y : T} (f : Y ⟶ X) : (mk f).left = Y := rfl
@[simp] lemma mk_hom {X Y : T} (f : Y ⟶ X) : (mk f).hom = f := rfl

def hom_mk {U V : over X} (f : U.left ⟶ V.left) (w : f ≫ V.hom = U.hom . obviously) :
U ⟶ V :=
{ left := f }

@[simp] lemma hom_mk_left {U V : over X} (f : U.left ⟶ V.left) (w : f ≫ V.hom = U.hom) :
(hom_mk f).left = f :=
rfl

def forget : (over X) ⥤ T := comma.fst _ _

@[simp] lemma forget_obj {U : over X} : forget.obj U = U.left := rfl
@[simp] lemma forget_map {U V : over X} {f : U ⟶ V} : forget.map f = f.left := rfl

def map {Y : T} (f : X ⟶ Y) : over X ⥤ over Y := comma.map_right _ $ functor.of.map f

section
variables {Y : T} {f : X ⟶ Y} {U V : over X} {g : U ⟶ V}
@[simp] lemma map_obj_left : ((map f).obj U).left = U.left := rfl
@[simp] lemma map_obj_hom : ((map f).obj U).hom = U.hom ≫ f := rfl
@[simp] lemma map_map_left : ((map f).map g).left = g.left := rfl
end

section
variables {D : Type u₃} [Dcat : category.{v₃} D]
include Dcat

def post (F : T ⥤ D) : over X ⥤ over (F.obj X) :=
{ obj := λ Y, mk $ F.map Y.hom,
map := λ Y₁ Y₂ f,
{ left := F.map f.left,
w' := by tidy; erw [← F.map_comp, w] } }

end

end over

def under (X : T) := comma.{0 v₃ v₃} (functor.of.obj X) (functor.id T)

namespace under

variables {X : T}

instance : category (under X) := by delta under; apply_instance

@[extensionality] lemma under_morphism.ext {X : T} {U V : under X} {f g : U ⟶ V}
(h : f.right = g.right) : f = g :=
by tidy

@[simp] lemma under_left (U : under X) : U.left = punit.star := by tidy
@[simp] lemma under_morphism_left {U V : under X} (f : U ⟶ V) : f.left = 𝟙 punit.star := by tidy

@[simp] lemma id_right (U : under X) : comma_morphism.right (𝟙 U) = 𝟙 U.right := rfl
@[simp] lemma comp_right (a b c : under X) (f : a ⟶ b) (g : b ⟶ c) :
(f ≫ g).right = f.right ≫ g.right := rfl

@[simp] lemma w {A B : under X} (f : A ⟶ B) : A.hom ≫ f.right = B.hom :=
by have := f.w; tidy

def mk {X Y : T} (f : X ⟶ Y) : under X :=
{ right := Y, hom := f }

@[simp] lemma mk_right {X Y : T} (f : X ⟶ Y) : (mk f).right = Y := rfl
@[simp] lemma mk_hom {X Y : T} (f : X ⟶ Y) : (mk f).hom = f := rfl

def hom_mk {U V : under X} (f : U.right ⟶ V.right) (w : U.hom ≫ f = V.hom . obviously) :
U ⟶ V :=
{ right := f }

@[simp] lemma hom_mk_right {U V : under X} (f : U.right ⟶ V.right) (w : U.hom ≫ f = V.hom) :
(hom_mk f).right = f :=
rfl

def forget : (under X) ⥤ T := comma.snd _ _

@[simp] lemma forget_obj {U : under X} : forget.obj U = U.right := rfl
@[simp] lemma forget_map {U V : under X} {f : U ⟶ V} : forget.map f = f.right := rfl

def map {Y : T} (f : X ⟶ Y) : under Y ⥤ under X := comma.map_left _ $ functor.of.map f

section
variables {Y : T} {f : X ⟶ Y} {U V : under Y} {g : U ⟶ V}
@[simp] lemma map_obj_right : ((map f).obj U).right = U.right := rfl
@[simp] lemma map_obj_hom : ((map f).obj U).hom = f ≫ U.hom := rfl
@[simp] lemma map_map_right : ((map f).map g).right = g.right := rfl
end

section
variables {D : Type u₃} [Dcat : category.{v₃} D]
include Dcat

def post {X : T} (F : T ⥤ D) : under X ⥤ under (F.obj X) :=
{ obj := λ Y, mk $ F.map Y.hom,
map := λ Y₁ Y₂ f,
{ right := F.map f.right,
w' := by tidy; erw [← F.map_comp, w] } }

end

end under

end category_theory
154 changes: 154 additions & 0 deletions category_theory/limits/over.lean
@@ -0,0 +1,154 @@
-- Copyright (c) 2018 Scott Morrison. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Authors: Johan Commelin, Reid Barton

import category_theory.comma
import category_theory.limits.preserves

universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation

open category_theory category_theory.limits

variables {J : Type v} [small_category J]
variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞
variable {X : C}

namespace category_theory.functor

def to_cocone (F : J ⥤ over X) : cocone (F ⋙ over.forget) :=
{ X := X,
ι := { app := λ j, (F.obj j).hom } }

@[simp] lemma to_cocone_X (F : J ⥤ over X) : F.to_cocone.X = X := rfl
@[simp] lemma to_cocone_ι (F : J ⥤ over X) (j : J) : F.to_cocone.ι.app j = (F.obj j).hom := rfl

def to_cone (F : J ⥤ under X) : cone (F ⋙ under.forget) :=
{ X := X,
π := { app := λ j, (F.obj j).hom } }

@[simp] lemma to_cone_X (F : J ⥤ under X) : F.to_cone.X = X := rfl
@[simp] lemma to_cone_π (F : J ⥤ under X) (j : J) : F.to_cone.π.app j = (F.obj j).hom := rfl

end category_theory.functor

namespace category_theory.over

def colimit (F : J ⥤ over X) [has_colimit (F ⋙ forget)] : cocone F :=
{ X := mk $ colimit.desc (F ⋙ forget) F.to_cocone,
ι :=
{ app := λ j, hom_mk $ colimit.ι (F ⋙ forget) j,
naturality' :=
begin
intros j j' f,
have := colimit.w (F ⋙ forget) f,
tidy
end } }

@[simp] lemma colimit_X_hom (F : J ⥤ over X) [has_colimit (F ⋙ forget)] :
((colimit F).X).hom = colimit.desc (F ⋙ forget) F.to_cocone := rfl
@[simp] lemma colimit_ι_app (F : J ⥤ over X) [has_colimit (F ⋙ forget)] (j : J) :
((colimit F).ι).app j = hom_mk (colimit.ι (F ⋙ forget) j) := rfl

def forget_colimit_is_colimit (F : J ⥤ over X) [has_colimit (F ⋙ forget)] :
is_colimit (forget.map_cocone (colimit F)) :=
is_colimit.of_iso_colimit (colimit.is_colimit (F ⋙ forget)) (cocones.ext (iso.refl _) (by tidy))

instance : reflects_colimits (forget : over X ⥤ C) :=
λ J 𝒥 F, by constructor; exactI λ t ht,
{ desc := λ s, hom_mk (ht.desc (forget.map_cocone s))
begin
apply ht.hom_ext, intro j,
rw [←category.assoc, ht.fac],
transitivity (F.obj j).hom,
exact w (s.ι.app j), -- TODO: How to write (s.ι.app j).w?
exact (w (t.ι.app j)).symm,
end,
fac' := begin
intros s j, ext, exact ht.fac (forget.map_cocone s) j
-- TODO: Ask Simon about multiple ext lemmas for defeq types (comma_morphism & over.category.hom)
end,
uniq' :=
begin
intros s m w,
ext1 j,
exact ht.uniq (forget.map_cocone s) m.left (λ j, congr_arg comma_morphism.left (w j))
end }

instance has_colimit {F : J ⥤ over X} [has_colimit (F ⋙ forget)] : has_colimit F :=
{ cocone := colimit F,
is_colimit := reflects_colimit.reflects (forget_colimit_is_colimit F) }

instance has_colimits_of_shape [has_colimits_of_shape J C] :
has_colimits_of_shape J (over X) :=
λ F, infer_instance

instance has_colimits [has_colimits C] : has_colimits (over X) :=
λ J 𝒥, by resetI; apply_instance

instance forget_preserves_colimits [has_colimits C] {X : C} :
preserves_colimits (forget : over X ⥤ C) :=
λ J 𝒥 F, by exactI
preserves_colimit_of_preserves_colimit_cocone (colimit.is_colimit F) (forget_colimit_is_colimit F)

end category_theory.over

namespace category_theory.under

def limit (F : J ⥤ under X) [has_limit (F ⋙ forget)] : cone F :=
{ X := mk $ limit.lift (F ⋙ forget) F.to_cone,
π :=
{ app := λ j, hom_mk $ limit.π (F ⋙ forget) j,
naturality' :=
begin
intros j j' f,
have := (limit.w (F ⋙ forget) f).symm,
tidy
end } }

@[simp] lemma limit_X_hom (F : J ⥤ under X) [has_limit (F ⋙ forget)] :
((limit F).X).hom = limit.lift (F ⋙ forget) F.to_cone := rfl
@[simp] lemma limit_π_app (F : J ⥤ under X) [has_limit (F ⋙ forget)] (j : J) :
((limit F).π).app j = hom_mk (limit.π (F ⋙ forget) j) := rfl

def forget_limit_is_limit (F : J ⥤ under X) [has_limit (F ⋙ forget)] :
is_limit (forget.map_cone (limit F)) :=
is_limit.of_iso_limit (limit.is_limit (F ⋙ forget)) (cones.ext (iso.refl _) (by tidy))

instance : reflects_limits (forget : under X ⥤ C) :=
λ J 𝒥 F, by constructor; exactI λ t ht,
{ lift := λ s, hom_mk (ht.lift (forget.map_cone s))
begin
apply ht.hom_ext, intro j,
rw [category.assoc, ht.fac],
transitivity (F.obj j).hom,
exact w (s.π.app j),
exact (w (t.π.app j)).symm,
end,
fac' := begin
intros s j, ext, exact ht.fac (forget.map_cone s) j
end,
uniq' :=
begin
intros s m w,
ext1 j,
exact ht.uniq (forget.map_cone s) m.right (λ j, congr_arg comma_morphism.right (w j))
end }

instance has_limit {F : J ⥤ under X} [has_limit (F ⋙ forget)] : has_limit F :=
{ cone := limit F,
is_limit := reflects_limit.reflects (forget_limit_is_limit F) }

instance has_limits_of_shape [has_limits_of_shape J C] :
has_limits_of_shape J (under X) :=
λ F, infer_instance

instance has_limits [has_limits C] : has_limits (under X) :=
λ J 𝒥, by resetI; apply_instance

instance forget_preserves_limits [has_limits C] {X : C} :
preserves_limits (forget : under X ⥤ C) :=
λ J 𝒥 F, by exactI
preserves_limit_of_preserves_limit_cone (limit.is_limit F) (forget_limit_is_limit F)

end category_theory.under

0 comments on commit 5c323cd

Please sign in to comment.