Skip to content

Commit

Permalink
feat(category_theory/limits): dualise a limits result (leanprover-com…
Browse files Browse the repository at this point in the history
…munity#2940)

Add the dual of `is_limit.of_cone_equiv`.

Co-authored-by: Scott Morrison <scott@tqft.net>
  • Loading branch information
2 people authored and cipher1024 committed Mar 15, 2022
1 parent 6636896 commit 4db9931
Show file tree
Hide file tree
Showing 5 changed files with 50 additions and 13 deletions.
9 changes: 9 additions & 0 deletions src/category_theory/adjunction/basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,15 @@ is_right_adjoint.left R
def right_adjoint (L : C ⥤ D) [is_left_adjoint L] : D ⥤ C :=
is_left_adjoint.right L

/-- The adjunction associated to a functor known to be a left adjoint. -/
def adjunction.of_left_adjoint (left : C ⥤ D) [is_left_adjoint left] :
adjunction left (right_adjoint left) :=
is_left_adjoint.adj
/-- The adjunction associated to a functor known to be a right adjoint. -/
def adjunction.of_right_adjoint (right : C ⥤ D) [is_right_adjoint right] :
adjunction (left_adjoint right) right :=
is_right_adjoint.adj

namespace adjunction

restate_axiom hom_equiv_unit'
Expand Down
10 changes: 5 additions & 5 deletions src/category_theory/limits/cones.lean
Original file line number Diff line number Diff line change
Expand Up @@ -257,12 +257,12 @@ by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obv
def precompose_id : precompose (𝟙 F) ≅ 𝟭 (cocone F) :=
by { fapply nat_iso.of_components, { intro s, fapply ext, refl, obviously }, obviously }

@[simps]
def precompose_equivalence {G : J ⥤ C} (α : G ≅ F) : cocone F ≌ cocone G :=
begin
refine equivalence.mk (precompose α.hom) (precompose α.inv) _ _,
{ symmetry, refine (precompose_comp _ _).symm.trans _, rw [iso.inv_hom_id], exact precompose_id },
{ refine (precompose_comp _ _).symm.trans _, rw [iso.hom_inv_id], exact precompose_id }
end
{ functor := precompose α.hom,
inverse := precompose α.inv,
unit_iso := nat_iso.of_components (λ s, cocones.ext (iso.refl _) (by tidy)) (by tidy),
counit_iso := nat_iso.of_components (λ s, cocones.ext (iso.refl _) (by tidy)) (by tidy) }

section
variable (F)
Expand Down
20 changes: 15 additions & 5 deletions src/category_theory/limits/limits.lean
Original file line number Diff line number Diff line change
Expand Up @@ -174,16 +174,15 @@ def iso_unique_cone_morphism {t : cone F} :
{ lift := λ s, (h s).default.hom,
uniq' := λ s f w, congr_arg cone_morphism.hom ((h s).uniq ⟨f, w⟩) } }

-- TODO: this should actually hold for an adjunction between cone F and cone G, not just for
-- equivalences
/--
Given two functors which have equivalent categories of cones, we can transport a limiting cone across
the equivalence.
-/
def of_cone_equiv {D : Type u'} [category.{v} D] {G : K ⥤ D} (h : cone F ≌ cone G) {c : cone G} (t : is_limit c) :
is_limit (h.inverse.obj c) :=
def of_cone_equiv {D : Type u'} [category.{v} D] {G : K ⥤ D}
(h : cone G ⥤ cone F) [is_right_adjoint h] {c : cone G} (t : is_limit c) :
is_limit (h.obj c) :=
mk_cone_morphism
(λ s, h.to_adjunction.hom_equiv s c (t.lift_cone_morphism _))
(λ s, (adjunction.of_right_adjoint h).hom_equiv s c (t.lift_cone_morphism _))
(λ s m, (adjunction.eq_hom_equiv_apply _ _ _).2 t.uniq_cone_morphism )

namespace of_nat_iso
Expand Down Expand Up @@ -396,6 +395,17 @@ def iso_unique_cocone_morphism {t : cocone F} :
{ desc := λ s, (h s).default.hom,
uniq' := λ s f w, congr_arg cocone_morphism.hom ((h s).uniq ⟨f, w⟩) } }

/--
Given two functors which have equivalent categories of cocones, we can transport a limiting cocone
across the equivalence.
-/
def of_cocone_equiv {D : Type u'} [category.{v} D] {G : K ⥤ D}
(h : cocone G ⥤ cocone F) [is_left_adjoint h] {c : cocone G} (t : is_colimit c) :
is_colimit (h.obj c) :=
mk_cocone_morphism
(λ s, ((adjunction.of_left_adjoint h).hom_equiv c s).symm (t.desc_cocone_morphism _))
(λ s m, (adjunction.hom_equiv_apply_eq _ _ _).1 t.uniq_cocone_morphism)

namespace of_nat_iso
variables {X : C} (h : coyoneda.obj (op X) ≅ F.cocones)

Expand Down
3 changes: 2 additions & 1 deletion src/category_theory/limits/over.lean
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,8 @@ def has_over_limit_discrete_of_wide_pullback_limit {B : C} {J : Type v} (F : dis
[has_limit (wide_pullback_diagram_of_diagram_over B F)] :
has_limit F :=
{ cone := _,
is_limit := is_limit.of_cone_equiv (cones_equiv B F).symm (limit.is_limit (wide_pullback_diagram_of_diagram_over B F)) }
is_limit := is_limit.of_cone_equiv
(cones_equiv B F).functor (limit.is_limit (wide_pullback_diagram_of_diagram_over B F)) }

/-- Given a wide pullback in `C`, construct a product in `C/B`. -/
def over_product_of_wide_pullback {J : Type v} [has_limits_of_shape.{v} (wide_pullback_shape J) C] {B : C} :
Expand Down
21 changes: 19 additions & 2 deletions src/category_theory/limits/preserves.lean
Original file line number Diff line number Diff line change
Expand Up @@ -129,9 +129,10 @@ def preserves_limit_of_iso {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K
preserves_limit K₂ F :=
{ preserves := λ c t,
begin
have t' := is_limit.of_cone_equiv (cones.postcompose_equivalence h) t,
have t' := is_limit.of_cone_equiv (cones.postcompose_equivalence h).inverse t,
let hF := iso_whisker_right h F,
have := is_limit.of_cone_equiv (cones.postcompose_equivalence hF).symm (preserves_limit.preserves t'),
have := is_limit.of_cone_equiv (cones.postcompose_equivalence hF).functor
(preserves_limit.preserves t'),
apply is_limit.of_iso_limit this,
refine cones.ext (iso.refl _) (λ j, _),
dsimp,
Expand All @@ -145,6 +146,22 @@ def preserves_colimit_of_preserves_colimit_cocone {F : C ⥤ D} {t : cocone K}
(h : is_colimit t) (hF : is_colimit (F.map_cocone t)) : preserves_colimit K F :=
⟨λ t' h', is_colimit.of_iso_colimit hF (functor.map_iso _ (is_colimit.unique_up_to_iso h h'))⟩

/-- Transfer preservation of colimits along a natural isomorphism in the shape. -/
def preserves_colimit_of_iso {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [preserves_colimit K₁ F] :
preserves_colimit K₂ F :=
{ preserves := λ c t,
begin
have t' := is_colimit.of_cocone_equiv (cocones.precompose_equivalence h).functor t,
let hF := iso_whisker_right h F,
have := is_colimit.of_cocone_equiv (cocones.precompose_equivalence hF).inverse
(preserves_colimit.preserves t'),
apply is_colimit.of_iso_colimit this,
refine cocones.ext (iso.refl _) (λ j, _),
dsimp,
rw [← F.map_comp],
simp,
end }

/-
A functor F : C → D reflects limits if whenever the image of a cone
under F is a limit cone in D, the cone was already a limit cone in C.
Expand Down

0 comments on commit 4db9931

Please sign in to comment.