[WIP] pi-clans

HoTTLean/ForMathlib.lean

@@ -533,35 +533,6 @@ lemma ofYoneda_isPullback {C : Type u} [Category.{v} C] {TL TR BL BR : C}
     · specialize h (some .right)
       exact h
 
-variable {C : Type u₁} [SmallCategory C] {F G : Cᵒᵖ ⥤ Type u₁}
-  (app : ∀ {X : C}, (yoneda.obj X ⟶ F) → (yoneda.obj X ⟶ G))
-  (naturality : ∀ {X Y : C} (f : X ⟶ Y) (α : yoneda.obj Y ⟶ F),
-    app (yoneda.map f ≫ α) = yoneda.map f ≫ app α)
-
-variable (F) in
-/--
-  A presheaf `F` on a small category `C` is isomorphic to
-  the hom-presheaf `Hom(y(•),F)`.
--/
-def yonedaIso : yoneda.op ⋙ yoneda.obj F ≅ F :=
-  NatIso.ofComponents (fun _ => Equiv.toIso yonedaEquiv)
-    (fun f => by ext : 1; dsimp; rw [yonedaEquiv_naturality'])
-
-def yonedaIsoMap : yoneda.op ⋙ yoneda.obj F ⟶ yoneda.op ⋙ yoneda.obj G where
-  app _ := app
-  naturality _ _ _ := by ext : 1; apply naturality
-
-/-- Build natural transformations between presheaves on a small category
-  by defining their action when precomposing by a morphism with
-  representable domain -/
-def NatTrans.yonedaMk : F ⟶ G :=
-  (yonedaIso F).inv ≫ yonedaIsoMap app naturality ≫ (yonedaIso G).hom
-
-theorem NatTrans.yonedaMk_app {X : C} (α : yoneda.obj X ⟶ F) :
-    α ≫ yonedaMk app naturality = app α := by
-  rw [← yonedaEquiv.apply_eq_iff_eq, yonedaEquiv_comp]
-  simp [yonedaMk, yonedaIso, yonedaIsoMap]
-
 namespace Functor
 
 theorem precomp_heq_of_heq_id {A B : Type u} {C : Type*} [Category.{v} A] [Category.{v} B] [Category C]
@@ -583,4 +554,89 @@ theorem comp_heq_of_heq_id {A B : Type u} {C : Type*} [Category.{v} A] [Category
 
 end Functor
 
+lemma eqToHom_heq_id {C : Type*} [Category C] (x y z : C) (h : x = y)
+    (hz : z = x) : eqToHom h ≍ 𝟙 z := by cat_disch
+
+lemma Cat.inv_heq_inv {C C' : Cat} (hC : C ≍ C') {X Y : C} {X' Y' : C'}
+    (hX : X ≍ X') (hY : Y ≍ Y') {f : X ⟶ Y} {f' : X' ⟶ Y'} (hf : f ≍ f') [IsIso f] :
+    have : IsIso f' := by aesop
+    inv f ≍ inv f' := by
+  subst hC hX hY hf
+  rfl
+
+lemma inv_heq_of_heq_inv {C : Grpd} {X Y X' Y' : C}
+    (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {g : Y' ⟶ X'} (hf : f ≍ inv g) :
+    inv f ≍ g := by
+  aesop_cat
+
+lemma inv_heq_inv {C : Type*} [Category C] {X Y : C} {X' Y' : C}
+    (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'} (hf : f ≍ f') [IsIso f] :
+    have : IsIso f' := by aesop
+    inv f ≍ inv f' := by
+  subst hX hY hf
+  rfl
+
+lemma Discrete.as_heq_as {α α' : Type u} (hα : α ≍ α') (x : Discrete α) (x' : Discrete α')
+    (hx : x ≍ x') : x.as ≍ x'.as := by
+  aesop_cat
+
+lemma Discrete.functor_ext' {X C : Type*} [Category C] {F G : X → C} (h : ∀ x : X, F x = G x) :
+    Discrete.functor F = Discrete.functor G := by
+  have : F = G := by aesop
+  subst this
+  rfl
+
+lemma Discrete.functor_eq {X C : Type*} [Category C] {F : Discrete X ⥤ C} :
+    F = Discrete.functor fun x ↦ F.obj ⟨x⟩ := by
+  fapply CategoryTheory.Functor.ext
+  · aesop
+  · intro x y f
+    cases x ; rcases f with ⟨⟨h⟩⟩
+    cases h
+    simp
+
+lemma Discrete.hext {X Y : Type u} (a : Discrete X) (b : Discrete Y) (hXY : X ≍ Y)
+    (hab : a.1 ≍ b.1) : a ≍ b := by
+  aesop_cat
+
+lemma Discrete.Hom.hext {α β : Type u} {x y : Discrete α} (x' y' : Discrete β) (hαβ : α ≍ β)
+    (hx : x ≍ x') (hy : y ≍ y') (f : x ⟶ y) (f' : x' ⟶ y') : f ≍ f' := by
+  aesop_cat
+
+open Prod in
+lemma Prod.sectR_comp_snd {C : Type u₁} [Category.{v₁} C] (Z : C)
+    (D : Type u₂) [Category.{v₂} D] : sectR Z D ⋙ snd C D = 𝟭 D :=
+  rfl
+
+section
+variable {C : Type u} [Category.{v} C] {D : Type u₁} [Category.{v₁} D] (P Q : ObjectProperty D)
+  (F : C ⥤ D) (hF : ∀ X, P (F.obj X))
+
+theorem ObjectProperty.lift_comp_inclusion_eq :
+    P.lift F hF ⋙ P.ι = F :=
+  rfl
+
+end
+
+lemma eqToHom_heq_eqToHom {C : Type*} [Category C] (x y x' y' : C) (hx : x = x')
+    (h : x = y) (h' : x' = y') : eqToHom h ≍ eqToHom h' := by aesop
+
 end CategoryTheory
+
+lemma hcongr_fun {α α' : Type u} (hα : α ≍ α') (β : α → Type v) (β' : α' → Type v) (hβ : β ≍ β')
+    (f : (x : α) → β x) (f' : (x : α') → β' x) (hf : f ≍ f')
+    {x : α} {x' : α'} (hx : x ≍ x') : f x ≍ f' x' := by
+  subst hα hβ hf hx
+  rfl
+
+lemma fun_hext {α α' : Type u} (hα : α ≍ α') (β : α → Type v) (β' : α' → Type v) (hβ : β ≍ β')
+    (f : (x : α) → β x) (f' : (x : α') → β' x)
+    (hf : {x : α} → {x' : α'} → (hx : x ≍ x') → f x ≍ f' x') : f ≍ f' := by
+  aesop
+
+lemma Subtype.hext {α α' : Sort u} (hα : α ≍ α') {p : α → Prop} {p' : α' → Prop}
+    (hp : p ≍ p') {a : { x // p x }} {a' : { x // p' x }} (ha : a.1 ≍ a'.1) : a ≍ a' := by
+  subst hα hp
+  simp only [heq_eq_eq]
+  ext
+  simpa [← heq_eq_eq]

HoTTLean/ForMathlib/CategoryTheory/Adjunction/Basic.lean

@@ -0,0 +1,49 @@
+import Mathlib.CategoryTheory.Adjunction.Basic
+
+namespace CategoryTheory
+
+open CategoryTheory.Functor NatIso Category
+
+-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
+universe v₁ v₂ v₃ u₁ u₂ u₃
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂}
+
+/-- The natural hom-set isomorphism `C(F(-),⋆) ≅ D(-,G(⋆))` given by an adjunction. -/
+def Adjunction.homIso [Category.{v₁} D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
+    yoneda ⋙ (Functor.whiskeringLeft _ _ _).obj (F.op) ≅ G ⋙ yoneda :=
+  NatIso.ofComponents
+  (fun X => (adj.representableBy X).toIso.symm)
+  (fun {X Y} f => by ext; simp [Functor.RepresentableBy.toIso, Functor.representableByEquiv,
+    adj.homEquiv_naturality_right])
+
+namespace Equivalence
+
+variable [Category.{v₂} D] {e : C ≌ D}
+
+def isoCompInverse {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D} (α : X ⋙ e.functor ≅ Y) :
+    X ≅ Y ⋙ e.inverse :=
+  calc X
+  _ ≅ X ⋙ 𝟭 _ := X.rightUnitor.symm
+  _ ≅ X ⋙ e.functor ⋙ e.inverse := Functor.isoWhiskerLeft X e.unitIso
+  _ ≅ (X ⋙ e.functor) ⋙ e.inverse := Functor.associator ..
+  _ ≅ Y ⋙ e.inverse := Functor.isoWhiskerRight α e.inverse
+
+@[simp]
+lemma isoCompInverse_hom_app {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D}
+    (α : X ⋙ e.functor ≅ Y) (A : J) :
+    (isoCompInverse α).hom.app A = e.unitIso.hom.app (X.obj A) ≫ e.inverse.map (α.hom.app A) := by
+  simp [isoCompInverse, Trans.trans]
+
+@[simp]
+lemma isoCompInverse_inv_app {J : Type*} [Category J] {X : J ⥤ C} {Y : J ⥤ D}
+    (α : X ⋙ e.functor ≅ Y) (A : J) :
+    (isoCompInverse α).inv.app A = e.inverse.map (α.inv.app A) ≫ e.unitIso.inv.app (X.obj A) := by
+  simp [isoCompInverse, Trans.trans]
+
+@[simps]
+def compFunctorNatIsoEquiv {J : Type*} [Category J] (X : J ⥤ C) (Y : J ⥤ D) :
+    (X ⋙ e.functor ≅ Y) ≃ (X ≅ Y ⋙ e.inverse) where
+  toFun := isoCompInverse
+  invFun α := (e.symm.isoCompInverse α.symm).symm
+  left_inv := by cat_disch
+  right_inv := by cat_disch

HoTTLean/ForMathlib/CategoryTheory/Adjunction/PartialAdjoint.lean

@@ -0,0 +1,66 @@
+import Mathlib.CategoryTheory.Adjunction.PartialAdjoint
+
+
+universe v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+namespace Functor
+
+open Category Opposite Limits
+
+section PartialRightAdjoint
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (F : C ⥤ D)
+
+structure PartialRightAdjoint (G : F.PartialRightAdjointSource ⥤ C) where
+  (repr : ∀ Y, (F.op ⋙ yoneda.obj Y.obj).RepresentableBy (G.obj Y))
+  (repr_homEquiv : ∀ X Y (f : X ⟶ Y), (repr Y).homEquiv (G.map f) =
+    (repr X).homEquiv (𝟙 _) ≫ f)
+
+@[simps]
+noncomputable def partialRightAdjoint.partialRightAdjoint :
+    PartialRightAdjoint F (partialRightAdjoint F) where
+  repr _ := Functor.representableBy _
+  repr_homEquiv _ _ _ := by
+    simp only [partialRightAdjoint_obj, comp_obj, op_obj, yoneda_obj_obj, partialRightAdjoint_map,
+      partialRightAdjointMap, partialRightAdjointHomEquiv]
+    erw [Equiv.apply_symm_apply]
+
+@[simps]
+noncomputable def rightAdjoint.partialRightAdjoint (L : C ⥤ D) [IsLeftAdjoint L] :
+    PartialRightAdjoint L (ObjectProperty.ι _ ⋙ rightAdjoint L) where
+  repr Y := Adjunction.representableBy (Adjunction.ofIsLeftAdjoint L) _
+  repr_homEquiv a b c := by
+    simp [Equiv.symm_apply_eq, Adjunction.homEquiv_naturality_right]
+
+lemma PartialRightAdjoint.repr_homEquiv_comp {G : F.PartialRightAdjointSource ⥤ C}
+    (P : PartialRightAdjoint F G) {X Y Z} (f : X ⟶ Y) (a : Z ⟶ G.obj X) :
+    (P.repr Y).homEquiv (a ≫ G.map f) = (P.repr X).homEquiv a ≫ f := by
+  have := (P.repr X).homEquiv_comp a (𝟙 _)
+  rw [(P.repr Y).homEquiv_comp, P.repr_homEquiv]
+  cat_disch
+
+lemma PartialRightAdjoint.repr_homEquiv_symm_comp {G : F.PartialRightAdjointSource ⥤ C}
+    (P : PartialRightAdjoint F G) {X Y Z} (f : X ⟶ Y) (a : F.obj Z ⟶ X.obj) :
+    (P.repr Y).homEquiv.symm (a ≫ f) = (P.repr X).homEquiv.symm a ≫ G.map f := by
+  rw [Equiv.symm_apply_eq, repr_homEquiv_comp, Equiv.apply_symm_apply]
+
+def PartialRightAdjoint.uniqueUpToIso {G G' : F.PartialRightAdjointSource ⥤ C}
+    (P : PartialRightAdjoint F G) (P' : PartialRightAdjoint F G') : G ≅ G' :=
+  NatIso.ofComponents (fun X => (P.repr _).uniqueUpToIso (P'.repr _))
+  (fun {X Y} f => by
+    apply yoneda.map_injective
+    ext Z a
+    simp only [yoneda_obj_obj, RepresentableBy.uniqueUpToIso_hom, comp_obj, op_obj, map_comp,
+      FullyFaithful.map_preimage, FunctorToTypes.comp, yoneda_map_app, NatIso.ofComponents_hom_app,
+      Function.comp_apply]
+    calc (P'.repr Y).homEquiv.symm ((P.repr Y).homEquiv (a ≫ G.map f))
+    _ = (P'.repr Y).homEquiv.symm ((P.repr X).homEquiv a ≫ f) := by
+      simpa using PartialRightAdjoint.repr_homEquiv_comp ..
+    _ = (P'.repr X).homEquiv.symm ((P.repr X).homEquiv a) ≫ G'.map f := by
+      apply repr_homEquiv_symm_comp)
+
+noncomputable abbrev isoPartialRightAdjoint (G : F.PartialRightAdjointSource ⥤ C)
+    (P : PartialRightAdjoint F G) : G ≅ partialRightAdjoint F :=
+    PartialRightAdjoint.uniqueUpToIso _ P (partialRightAdjoint.partialRightAdjoint _)

HoTTLean/ForMathlib/CategoryTheory/Bicategory/Grothendieck.lean

@@ -585,6 +585,43 @@ def toTransport_fiber (x : ∫ F) {c : C} (t : x.base ⟶ c) :
     (toTransport x t).fiber = 𝟙 _ :=
   rfl
 
+lemma transport_id {x : ∫ F} :
+    transport x (𝟙 x.base) = x := by
+  fapply Grothendieck.ext <;> simp [transport]
+
+lemma transport_eqToHom {X: C} {X' : ∫ F} (hX': (forget F).obj X' = X):
+    X'.transport (eqToHom hX') = X' := by
+  subst hX'
+  simp [transport_id]
+
+lemma toTransport_id {X : ∫ F} :
+    toTransport X (𝟙 X.base) = eqToHom transport_id.symm := by
+  apply Grothendieck.Hom.ext <;> simp
+
+lemma toTransport_eqToHom {X: C} {X' : ∫ F} (hX': (forget F).obj X' = X):
+    toTransport X' (eqToHom hX') = eqToHom (by subst hX'; simp[transport_id]) := by
+  subst hX'
+  simp [toTransport_id]
+
+lemma transport_comp (x : ∫ F) {c d: C} (t : x.base ⟶ c) (t': c ⟶ d):
+      transport x (t ≫ t') = transport (c:= d) (transport x t) t' := by
+  simp [transport]
+
+lemma toTransport_comp (x : ∫ F) {c d: C} (t : x.base ⟶ c) (t': c ⟶ d):
+    toTransport x (t ≫ t') =
+    toTransport x t ≫ toTransport (transport x t) t' ≫ eqToHom (transport_comp x t t').symm := by
+  simp only [← Category.assoc, ← heq_eq_eq, heq_comp_eqToHom_iff]
+  simp only [toTransport, transport_base, transport_fiber]
+  fapply Grothendieck.Hom.hext'
+  · rfl
+  · rfl
+  · simp [transport_comp]
+  · simp
+  · simp only [transport_base, Hom.mk_base, transport_fiber, Hom.comp_base, Hom.comp_fiber, map_id,
+      Category.comp_id]
+    symm
+    apply eqToHom_heq_id_dom
+
 /--
 Construct an isomorphism in a Grothendieck construction from isomorphisms in its base and fiber.
 -/
@@ -851,6 +888,14 @@ lemma toPseudoFunctor'Iso.inv_comp_forget : toPseudoFunctor'Iso.inv F ⋙ forget
     Pseudofunctor.Grothendieck.forget _ :=
   rfl
 
+lemma map_eq_pseudofunctor_map {G} (α : F ⟶ G) : map α = (toPseudoFunctor'Iso F).hom ⋙
+    Pseudofunctor.Grothendieck.map α.toStrongTrans' ⋙
+    (toPseudoFunctor'Iso G).inv := by
+  fapply Functor.ext
+  · aesop
+  · intro _
+    aesop
+
 end Pseudofunctor
 
 section
@@ -1146,7 +1191,7 @@ include hom_id in
 lemma functorFromCompHom_id (c : C) : functorFromCompHom fib hom G (𝟙 c)
     = eqToHom (by simp [Cat.id_eq_id, Functor.id_comp]) := by
   ext x
-  simp [hom_id, functorFromCompHom]
+  simp [hom_id, eqToHom_map, functorFromCompHom]
 
 include hom_comp in
 lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂ ⟶ c₃):
@@ -1155,7 +1200,7 @@ lemma functorFromCompHom_comp (c₁ c₂ c₃ : C) (f : c₁ ⟶ c₂) (g : c₂
     Functor.whiskerLeft (F.map f) (functorFromCompHom fib hom G g) ≫
     eqToHom (by simp[Cat.comp_eq_comp, Functor.map_comp, Functor.assoc]) := by
   ext
-  simp [functorFromCompHom, hom_comp]
+  simp [functorFromCompHom, hom_comp, eqToHom_map]
 
 theorem functorFrom_comp : functorFrom fib hom hom_id hom_comp ⋙ G =
     functorFrom (functorFromCompFib fib G) (functorFromCompHom fib hom G)
@@ -1390,6 +1435,55 @@ def mapWhiskerRightAsSmallFunctor (α : F ⟶ G) :
 
 end AsSmall
 
+noncomputable section
+
+variable {F} {x y : ∫ F} (f : x ⟶ y) [IsIso f]
+
+instance : IsIso f.base := by
+  refine ⟨ (CategoryTheory.inv f).base , ?_, ?_ ⟩
+  · simp [← Grothendieck.Hom.comp_base]
+  · simp [← Grothendieck.Hom.comp_base]
+
+def invFiber : y.fiber ⟶ (F.map f.base).obj x.fiber :=
+  eqToHom (by simp [← Functor.comp_obj, ← Cat.comp_eq_comp, ← Functor.map_comp,
+      ← Grothendieck.Hom.comp_base]) ≫
+    (F.map f.base).map (CategoryTheory.inv f).fiber
+
+@[simp]
+lemma fiber_comp_invFiber : f.fiber ≫ invFiber f = 𝟙 ((F.map f.base).obj x.fiber) := by
+  have h := Functor.Grothendieck.Hom.comp_fiber f (CategoryTheory.inv f)
+  rw! [IsIso.hom_inv_id] at h
+  have h0 : F.map (CategoryTheory.inv f).base ⋙ F.map f.base = 𝟭 _ := by
+    simp [← Cat.comp_eq_comp, ← Functor.map_comp, ← Grothendieck.Hom.comp_base, Cat.id_eq_id]
+  have h1 := Functor.congr_map (F.map f.base) h
+  simp [← heq_eq_eq, eqToHom_map, ← Functor.comp_map, Functor.congr_hom h0] at h1
+  dsimp [invFiber]
+  rw! [← h1]
+  simp
+
+@[simp]
+lemma invFiber_comp_fiber : invFiber f ≫ f.fiber = 𝟙 _ := by
+  have h := Functor.Grothendieck.Hom.comp_fiber (CategoryTheory.inv f) f
+  rw! [IsIso.inv_hom_id] at h
+  simp [invFiber]
+  convert h.symm
+  · simp
+  · simp
+  · simpa using (eqToHom_heq_id_cod _ _ _).symm
+
+instance : IsIso f.fiber :=
+  ⟨invFiber f , fiber_comp_invFiber f, invFiber_comp_fiber f⟩
+
+lemma inv_base : CategoryTheory.inv f.base = Grothendieck.Hom.base (CategoryTheory.inv f) := by
+  apply IsIso.inv_eq_of_hom_inv_id
+  simp [← Hom.comp_base]
+
+lemma inv_fiber : CategoryTheory.inv f.fiber = invFiber f := by
+  apply IsIso.inv_eq_of_hom_inv_id
+  simp
+
+end
+
 end Grothendieck
 
 end Functor