Skip to content

Commit 379a2ae

Browse files
urkudint-y1Scott Morrison
committed
feat: port CategoryTheory.Closed.Functor (#4922)
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
1 parent bbc68ef commit 379a2ae

File tree

5 files changed

+247
-5
lines changed

5 files changed

+247
-5
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -794,6 +794,7 @@ import Mathlib.CategoryTheory.Category.RelCat
794794
import Mathlib.CategoryTheory.Category.TwoP
795795
import Mathlib.CategoryTheory.Category.ULift
796796
import Mathlib.CategoryTheory.Closed.Cartesian
797+
import Mathlib.CategoryTheory.Closed.Functor
797798
import Mathlib.CategoryTheory.Closed.FunctorCategory
798799
import Mathlib.CategoryTheory.Closed.Monoidal
799800
import Mathlib.CategoryTheory.Closed.Types

‎Mathlib/CategoryTheory/Closed/Functor.lean‎

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
/-
2+
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Bhavik Mehta
5+
6+
! This file was ported from Lean 3 source module category_theory.closed.functor
7+
! leanprover-community/mathlib commit cea27692b3fdeb328a2ddba6aabf181754543184
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.CategoryTheory.Closed.Cartesian
12+
import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
13+
import Mathlib.CategoryTheory.Adjunction.FullyFaithful
14+
15+
/-!
16+
# Cartesian closed functors
17+
18+
Define the exponential comparison morphisms for a functor which preserves binary products, and use
19+
them to define a cartesian closed functor: one which (naturally) preserves exponentials.
20+
21+
Define the Frobenius morphism, and show it is an isomorphism iff the exponential comparison is an
22+
isomorphism.
23+
24+
## TODO
25+
Some of the results here are true more generally for closed objects and for closed monoidal
26+
categories, and these could be generalised.
27+
28+
## References
29+
https://ncatlab.org/nlab/show/cartesian+closed+functor
30+
https://ncatlab.org/nlab/show/Frobenius+reciprocity
31+
32+
## Tags
33+
Frobenius reciprocity, cartesian closed functor
34+
35+
-/
36+
37+
38+
noncomputable section
39+
40+
namespace CategoryTheory
41+
42+
open Category Limits CartesianClosed
43+
44+
universe v u u'
45+
46+
variable {C : Type u} [Category.{v} C]
47+
48+
variable {D : Type u'} [Category.{v} D]
49+
50+
variable [HasFiniteProducts C] [HasFiniteProducts D]
51+
52+
variable (F : C ⥤ D) {L : D ⥤ C}
53+
54+
/-- The Frobenius morphism for an adjunction `L ⊣ F` at `A` is given by the morphism
55+
56+
L(FA ⨯ B) ⟶ LFA ⨯ LB ⟶ A ⨯ LB
57+
58+
natural in `B`, where the first morphism is the product comparison and the latter uses the counit
59+
of the adjunction.
60+
61+
We will show that if `C` and `D` are cartesian closed, then this morphism is an isomorphism for all
62+
`A` iff `F` is a cartesian closed functor, i.e. it preserves exponentials.
63+
-/
64+
def frobeniusMorphism (h : L ⊣ F) (A : C) :
65+
prod.functor.obj (F.obj A) ⋙ L ⟶ L ⋙ prod.functor.obj A :=
66+
prodComparisonNatTrans L (F.obj A) ≫ whiskerLeft _ (prod.functor.map (h.counit.app _))
67+
#align category_theory.frobenius_morphism CategoryTheory.frobeniusMorphism
68+
69+
/-- If `F` is full and faithful and has a left adjoint `L` which preserves binary products, then the
70+
Frobenius morphism is an isomorphism.
71+
-/
72+
instance frobeniusMorphism_iso_of_preserves_binary_products (h : L ⊣ F) (A : C)
73+
[PreservesLimitsOfShape (Discrete WalkingPair) L] [Full F] [Faithful F] :
74+
IsIso (frobeniusMorphism F h A) :=
75+
suffices ∀ (X : D), IsIso ((frobeniusMorphism F h A).app X) from NatIso.isIso_of_isIso_app _
76+
fun B ↦ by dsimp [frobeniusMorphism]; infer_instance
77+
#align category_theory.frobenius_morphism_iso_of_preserves_binary_products CategoryTheory.frobeniusMorphism_iso_of_preserves_binary_products
78+
79+
variable [CartesianClosed C] [CartesianClosed D]
80+
81+
variable [PreservesLimitsOfShape (Discrete WalkingPair) F]
82+
83+
/-- The exponential comparison map.
84+
`F` is a cartesian closed functor if this is an iso for all `A`.
85+
-/
86+
def expComparison (A : C) : exp A ⋙ F ⟶ F ⋙ exp (F.obj A) :=
87+
transferNatTrans (exp.adjunction A) (exp.adjunction (F.obj A)) (prodComparisonNatIso F A).inv
88+
#align category_theory.exp_comparison CategoryTheory.expComparison
89+
90+
theorem expComparison_ev (A B : C) :
91+
Limits.prod.map (𝟙 (F.obj A)) ((expComparison F A).app B) ≫ (exp.ev (F.obj A)).app (F.obj B) =
92+
inv (prodComparison F _ _) ≫ F.map ((exp.ev _).app _) := by
93+
convert transferNatTrans_counit _ _ (prodComparisonNatIso F A).inv B using 2
94+
apply IsIso.inv_eq_of_hom_inv_id -- Porting note: was `ext`
95+
simp only [Limits.prodComparisonNatIso_inv, asIso_inv, NatIso.isIso_inv_app, IsIso.hom_inv_id]
96+
#align category_theory.exp_comparison_ev CategoryTheory.expComparison_ev
97+
98+
theorem coev_expComparison (A B : C) :
99+
F.map ((exp.coev A).app B) ≫ (expComparison F A).app (A ⨯ B) =
100+
(exp.coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prodComparison F A B)) := by
101+
convert unit_transferNatTrans _ _ (prodComparisonNatIso F A).inv B using 3
102+
apply IsIso.inv_eq_of_hom_inv_id -- Porting note: was `ext`
103+
dsimp
104+
simp
105+
#align category_theory.coev_exp_comparison CategoryTheory.coev_expComparison
106+
107+
theorem uncurry_expComparison (A B : C) :
108+
CartesianClosed.uncurry ((expComparison F A).app B) =
109+
inv (prodComparison F _ _) ≫ F.map ((exp.ev _).app _) :=
110+
by rw [uncurry_eq, expComparison_ev]
111+
#align category_theory.uncurry_exp_comparison CategoryTheory.uncurry_expComparison
112+
113+
/-- The exponential comparison map is natural in `A`. -/
114+
theorem expComparison_whiskerLeft {A A' : C} (f : A' ⟶ A) :
115+
expComparison F A ≫ whiskerLeft _ (pre (F.map f)) =
116+
whiskerRight (pre f) _ ≫ expComparison F A' := by
117+
ext B
118+
dsimp
119+
apply uncurry_injective
120+
rw [uncurry_natural_left, uncurry_natural_left, uncurry_expComparison, uncurry_pre,
121+
prod.map_swap_assoc, ← F.map_id, expComparison_ev, ← F.map_id, ←
122+
prodComparison_inv_natural_assoc, ← prodComparison_inv_natural_assoc, ← F.map_comp, ←
123+
F.map_comp, prod_map_pre_app_comp_ev]
124+
#align category_theory.exp_comparison_whisker_left CategoryTheory.expComparison_whiskerLeft
125+
126+
/-- The functor `F` is cartesian closed (ie preserves exponentials) if each natural transformation
127+
`exp_comparison F A` is an isomorphism
128+
-/
129+
class CartesianClosedFunctor where
130+
comparison_iso : ∀ A, IsIso (expComparison F A)
131+
#align category_theory.cartesian_closed_functor CategoryTheory.CartesianClosedFunctor
132+
133+
attribute [instance] CartesianClosedFunctor.comparison_iso
134+
135+
theorem frobeniusMorphism_mate (h : L ⊣ F) (A : C) :
136+
transferNatTransSelf (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)
137+
(frobeniusMorphism F h A) =
138+
expComparison F A := by
139+
rw [← Equiv.eq_symm_apply]
140+
ext B : 2
141+
dsimp [frobeniusMorphism, transferNatTransSelf, transferNatTrans, Adjunction.comp]
142+
simp only [id_comp, comp_id]
143+
rw [← L.map_comp_assoc, prod.map_id_comp, assoc]
144+
-- Porting note: need to use `erw` here.
145+
erw [expComparison_ev]
146+
rw [prod.map_id_comp, assoc, ← F.map_id, ← prodComparison_inv_natural_assoc, ← F.map_comp]
147+
-- Porting note: need to use `erw` here.
148+
erw [exp.ev_coev]
149+
rw [F.map_id (A ⨯ L.obj B), comp_id]
150+
apply prod.hom_ext
151+
· rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_fst]
152+
simp
153+
· rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_snd]
154+
simp
155+
#align category_theory.frobenius_morphism_mate CategoryTheory.frobeniusMorphism_mate
156+
157+
/--
158+
If the exponential comparison transformation (at `A`) is an isomorphism, then the Frobenius morphism
159+
at `A` is an isomorphism.
160+
-/
161+
theorem frobeniusMorphism_iso_of_expComparison_iso (h : L ⊣ F) (A : C)
162+
[i : IsIso (expComparison F A)] : IsIso (frobeniusMorphism F h A) := by
163+
rw [← frobeniusMorphism_mate F h] at i
164+
exact @transferNatTransSelf_of_iso _ _ _ _ _ _ _ _ _ _ _ i
165+
#align category_theory.frobenius_morphism_iso_of_exp_comparison_iso CategoryTheory.frobeniusMorphism_iso_of_expComparison_iso
166+
167+
/--
168+
If the Frobenius morphism at `A` is an isomorphism, then the exponential comparison transformation
169+
(at `A`) is an isomorphism.
170+
-/
171+
theorem expComparison_iso_of_frobeniusMorphism_iso (h : L ⊣ F) (A : C)
172+
[i : IsIso (frobeniusMorphism F h A)] : IsIso (expComparison F A) := by
173+
rw [← frobeniusMorphism_mate F h]; infer_instance
174+
#align category_theory.exp_comparison_iso_of_frobenius_morphism_iso CategoryTheory.expComparison_iso_of_frobeniusMorphism_iso
175+
176+
/-- If `F` is full and faithful, and has a left adjoint which preserves binary products, then it is
177+
cartesian closed.
178+
179+
TODO: Show the converse, that if `F` is cartesian closed and its left adjoint preserves binary
180+
products, then it is full and faithful.
181+
-/
182+
def cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts (h : L ⊣ F) [Full F] [Faithful F]
183+
[PreservesLimitsOfShape (Discrete WalkingPair) L] : CartesianClosedFunctor F where
184+
comparison_iso _ := expComparison_iso_of_frobeniusMorphism_iso F h _
185+
#align category_theory.cartesian_closed_functor_of_left_adjoint_preserves_binary_products CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts
186+
187+
end CategoryTheory

‎Mathlib/CategoryTheory/Iso.lean‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -315,13 +315,19 @@ noncomputable def asIso (f : X ⟶ Y) [IsIso f] : X ≅ Y :=
315315
⟨f, inv f, hom_inv_id f, inv_hom_id f⟩
316316
#align category_theory.as_iso CategoryTheory.asIso
317317

318+
-- Porting note: the `IsIso f` argument had been instance implicit,
319+
-- but we've changed it to implicit as a `rw` in `Mathlib.CategoryTheory.Closed.Functor`
320+
-- was failing to generate it by typeclass search.
318321
@[simp]
319-
theorem asIso_hom (f : X ⟶ Y) [IsIso f] : (asIso f).hom = f :=
322+
theorem asIso_hom (f : X ⟶ Y) {_ : IsIso f} : (asIso f).hom = f :=
320323
rfl
321324
#align category_theory.as_iso_hom CategoryTheory.asIso_hom
322325

326+
-- Porting note: the `IsIso f` argument had been instance implicit,
327+
-- but we've changed it to implicit as a `rw` in `Mathlib.CategoryTheory.Closed.Functor`
328+
-- was failing to generate it by typeclass search.
323329
@[simp]
324-
theorem asIso_inv (f : X ⟶ Y) [IsIso f] : (asIso f).inv = inv f :=
330+
theorem asIso_inv (f : X ⟶ Y) {_ : IsIso f} : (asIso f).inv = inv f :=
325331
rfl
326332
#align category_theory.as_iso_inv CategoryTheory.asIso_inv
327333

0 commit comments

Comments
 (0)