Skip to content

Commit 440fcf3

Browse files
fwethfweth
committed
...
1 parent 5d6c205 commit 440fcf3

1 file changed

Lines changed: 45 additions & 28 deletions

File tree

β€ŽMathlib/CategoryTheory/Closed/PowerObjects.leanβ€Ž

Lines changed: 45 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -25,52 +25,69 @@ variable {β„° : Type u} [Category.{v} β„°]
2525

2626
namespace LeftRepresentable
2727

28-
variable (F : (β„° Γ— β„°)α΅’α΅– β₯€ Type (max u v))
28+
variable (F : β„°α΅’α΅– β₯€ β„°α΅’α΅– β₯€ Type (max u v))
2929

30-
abbrev fixedLeft (B : β„°) : β„°α΅’α΅– β₯€ Type (max u v) :=
31-
(curryObj ((prodOpEquiv β„°).inverse β‹™ F)).obj (op B)
30+
variable {F} {B PB : β„°} (hPB : (F.obj (op B)).RepresentableBy PB)
31+
{C PC : β„°} (hPC : (F.obj (op C)).RepresentableBy PC)
3232

33-
def curryObj' : β„°α΅’α΅– β₯€ β„°α΅’α΅– β₯€ Type (max u v) := curryObj ((prodOpEquiv β„°).inverse β‹™ F)
33+
abbrev uEl hP := hP.homEquiv (πŸ™ PB)
3434

35-
variable {F} {B PB : β„°} (hPB : (fixedLeft F B).RepresentableBy PB)
36-
{C PC : β„°} (hPC : ((curryObj' F).obj (op C)).RepresentableBy PC)
37-
38-
/-- The morphism induced by a morphism between the base objects. -/
3935
def Pmap (h : B ⟢ C) : PC ⟢ PB :=
40-
hPB.homEquiv.symm (F.map (h Γ—β‚˜ πŸ™ PC).op (hPC.homEquiv (πŸ™ PC)))
36+
hPB.homEquiv.symm ((F.map h.op).app (op PC) uElC)
4137

42-
lemma map_universal (h : B ⟢ C) :
43-
F.map (πŸ™ B Γ—β‚˜ (Pmap hPB hPC h)).op (hPB.homEquiv (πŸ™ PB))
44-
= F.map (h Γ—β‚˜ πŸ™ PC).op (hPC.homEquiv (πŸ™ PC)) := by
38+
@[simp]
39+
lemma Pmap_universal (h : B ⟢ C) :
40+
(F.obj (op B)).map (Pmap hPB hPC h).op (hPB.homEquiv (πŸ™ PB)) =
41+
(F.map h.op).app (op PC) (hPC.homEquiv (πŸ™ PC)) := by
4542
calc
46-
_ = (fixedLeft F B).map (Pmap hPB hPC h).op (hPB.homEquiv (πŸ™ PB)) := by rfl
47-
_ = F.map (h Γ—β‚˜ πŸ™ PC).op (hPC.homEquiv (πŸ™ PC)) := by
48-
rw [← hPB.homEquiv_eq, Pmap, hPB.homEquiv.apply_symm_apply]
43+
_ = hPB.homEquiv (Pmap hPB hPC h) := by rw [← hPB.homEquiv_eq]
44+
_ = (F.map h.op).app (op PC) (hPC.homEquiv (πŸ™ PC)) := by simp [Pmap]
4945

50-
variable {D PD : β„°} (hPD : ((curryObj' F).obj (op D)).RepresentableBy PD)
46+
variable {D PD : β„°} (hPD : (F.obj (op D)).RepresentableBy PD)
5147

5248
lemma comm {PB PC : β„°} (f : B ⟢ C) (Pf : PC ⟢ PB) :
5349
(f Γ—β‚˜ πŸ™ PB).op ≫ (πŸ™ B Γ—β‚˜ Pf).op = (πŸ™ C Γ—β‚˜ Pf).op ≫ (f Γ—β‚˜ πŸ™ PC).op :=
5450
congrArg Quiver.Hom.op (by simp)
5551

5652
lemma compose (h : B ⟢ C) (h' : C ⟢ D) :
5753
Pmap hPB hPD (h ≫ h') = Pmap hPC hPD h' ≫ Pmap hPB hPC h := by
58-
let F' := (prodOpEquiv β„°).inverse β‹™ F
5954
let Ph := Pmap hPB hPC h
6055
let Ph' := Pmap hPC hPD h'
6156
apply hPB.homEquiv.injective
6257
calc
63-
_ = F.map ((h Γ—β‚˜ πŸ™ _) ≫ (h' Γ—β‚˜ πŸ™ _)).op (hPD.homEquiv (πŸ™ PD)) := by unfold Pmap; simp
64-
_ = F.map ((h' Γ—β‚˜ πŸ™ _).op ≫ (h Γ—β‚˜ πŸ™ _).op) (hPD.homEquiv (πŸ™ PD)) := by rw[op_comp]
65-
_ = F.map ((πŸ™ _ Γ—β‚˜ Ph').op ≫ (h Γ—β‚˜ πŸ™ _).op) (hPC.homEquiv (πŸ™ PC)) := by
66-
rw[FunctorToTypes.map_comp_apply, ← map_universal, ← FunctorToTypes.map_comp_apply];
67-
_ = F.map ((h Γ—β‚˜ πŸ™ _).op ≫ (πŸ™ _ Γ—β‚˜ Ph').op) (hPC.homEquiv (πŸ™ PC)) := by rw[comm]
68-
_ = F.map ((πŸ™ _ Γ—β‚˜ Ph).op ≫ (πŸ™ _ Γ—β‚˜ Ph').op) (hPB.homEquiv (πŸ™ PB)) := by
69-
rw[FunctorToTypes.map_comp_apply, ← map_universal, ← FunctorToTypes.map_comp_apply]
70-
_ = F.map (πŸ™ _ Γ—β‚˜ Ph' ≫ Ph).op (hPB.homEquiv (πŸ™ PB)) := by rw[comm_op]; simp
71-
_ = ((curryObj' F).obj _).map (Ph' ≫ Ph).op (hPB.homEquiv (πŸ™ PB)) := by
72-
rw[prod_comp, comp_id, op_comp]; simp only [curryObj]
73-
_ = hPB.homEquiv (Ph' ≫ Ph) := by rw[← hPB.homEquiv_eq]
58+
_ = (F.map (h ≫ h').op).app (op PD) (hPD.homEquiv (πŸ™ PD)) := by simp [Pmap]
59+
_ = (F.map h.op).app (op PD) ((F.map h'.op).app (op PD) (hPD.homEquiv (πŸ™ PD))) := by simp
60+
_ = (F.map h.op).app (op PD)
61+
((F.obj (op C)).map (Pmap hPC hPD h').op (hPC.homEquiv (πŸ™ PC))) := by
62+
simpa [Ph'] using
63+
congrArg (fun t => (F.map h.op).app (op PD) t) ((Pmap_universal hPC hPD h').symm)
64+
_ = (F.obj (op B)).map Ph'.op
65+
((F.map h.op).app (op PC) (hPC.homEquiv (πŸ™ PC))) := by
66+
simpa using congrArg (fun f => f (hPC.homEquiv (πŸ™ PC))) ((F.map h.op).naturality Ph'.op)
67+
_ = (F.obj (op B)).map Ph'.op
68+
((F.obj (op B)).map Ph.op (hPB.homEquiv (πŸ™ PB))) := by
69+
have hu := (Pmap_universal (F := F) (hPB := hPB) (hPC := hPC) h)
70+
have hu' := congrArg (fun t => (F.obj (op B)).map Ph'.op t) hu.symm
71+
simpa [Ph] using hu'
72+
_ = (F.obj (op B)).map (Ph.op ≫ Ph'.op) (hPB.homEquiv (πŸ™ PB)) := by
73+
simp [FunctorToTypes.map_comp_apply]
74+
_ = (F.obj (op B)).map ( (Ph' ≫ Ph).op ) (hPB.homEquiv (πŸ™ PB)) := by
75+
simp [op_comp]
76+
_ = hPB.homEquiv (Ph' ≫ Ph) := by
77+
simpa [Ph, Ph'] using
78+
(hPB.homEquiv_eq (Ph' ≫ Ph)).symm
79+
80+
81+
-- _ = F.map ((h' Γ—β‚˜ πŸ™ _).op ≫ (h Γ—β‚˜ πŸ™ _).op) (hPD.homEquiv (πŸ™ PD)) := by rw[op_comp]
82+
-- _ = F.map ((πŸ™ _ Γ—β‚˜ Ph').op ≫ (h Γ—β‚˜ πŸ™ _).op) (hPC.homEquiv (πŸ™ PC)) := by
83+
-- rw[FunctorToTypes.map_comp_apply, ← map_universal, ← FunctorToTypes.map_comp_apply];
84+
-- _ = F.map ((h Γ—β‚˜ πŸ™ _).op ≫ (πŸ™ _ Γ—β‚˜ Ph').op) (hPC.homEquiv (πŸ™ PC)) := by rw[comm]
85+
-- _ = F.map ((πŸ™ _ Γ—β‚˜ Ph).op ≫ (πŸ™ _ Γ—β‚˜ Ph').op) (hPB.homEquiv (πŸ™ PB)) := by
86+
-- rw[FunctorToTypes.map_comp_apply, ← map_universal, ← FunctorToTypes.map_comp_apply]
87+
-- _ = F.map (πŸ™ _ Γ—β‚˜ Ph' ≫ Ph).op (hPB.homEquiv (πŸ™ PB)) := by rw[comm_op]; simp
88+
-- _ = ((curryObj' F).obj _).map (Ph' ≫ Ph).op (hPB.homEquiv (πŸ™ PB)) := by
89+
-- rw[prod_comp, comp_id, op_comp]; simp only [curryObj]
90+
-- _ = hPB.homEquiv (Ph' ≫ Ph) := by rw[← hPB.homEquiv_eq]
7491

7592
/-- Let `F : β„°α΅’α΅– Γ— β„°α΅’α΅– β₯€ Type`. If for each `B` we choose an object `P B` representing
7693
the functor `C ↦ F (B, C)`, then these choices assemble into a covariant functor `β„°α΅’α΅– β₯€ β„°`. -/

0 commit comments

Comments
Β (0)