bump mathlib

InfinityCosmos/ForMathlib/AlgebraicTopology/HomotopyCat.lean

@@ -1,5 +1,5 @@
 import InfinityCosmos.Mathlib.AlgebraicTopology.Nerve
-import Mathlib.CategoryTheory.Category.Quiv
+import Mathlib.CategoryTheory.Category.ReflQuiv
 import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
 import Mathlib.CategoryTheory.Monad.Limits
 
@@ -11,15 +11,6 @@ universe v v₁ v₂ u u₁ u₂
 
 section
 
--- NB: Copied to Mathlib/CategoryTheory/Category/Cat.lean
-theorem Cat.id_eq_id (X : Cat) : 𝟙 X = 𝟭 X := rfl
-theorem Cat.comp_eq_comp {X Y Z : Cat} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙ G := rfl
-@[simp] theorem Cat.of_α (C) [Category C] : (of C).α = C := rfl
-
--- NB: Copied to mathlib/CategoryTheory/Category/Quiv.lean
-theorem Quiv.id_eq_id (X : Quiv) : 𝟙 X = 𝟭q X := rfl
-theorem Quiv.comp_eq_comp {X Y Z : Quiv} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙q G := rfl
-
 -- NB: Copied to Mathlib/CategoryTheory/Quotient.lean
 namespace Quotient
 variable {C : Type _} [Category C] (r : HomRel C)
@@ -49,323 +40,6 @@ theorem CompClosure.congruence : Congruence fun a b => Relation.EqvGen (@CompClo
 
 end Quotient
 
-
--- NB: Copied to ForMathlib/Combinatorics/Quiver/ReflQuiver.lean
-@[pp_with_univ]
-class ReflQuiver (obj : Type u) extends Quiver.{v} obj : Type max u v where
-  /-- The identity morphism on an object. -/
-  id : ∀ X : obj, Hom X X
-
-/-- Notation for the identity morphism in a category. -/
-scoped notation "𝟙rq" => ReflQuiver.id  -- type as \b1
-
-instance catToReflQuiver {C : Type u} [inst : Category.{v} C] : ReflQuiver.{v+1, u} C :=
-  { inst with }
-
-@[simp] theorem ReflQuiver.id_eq_id {C : Type*} [Category C] (X : C) : 𝟙rq X = 𝟙 X := rfl
-
-/-- A morphism of quivers. As we will later have categorical functors extend this structure,
-we call it a `Prefunctor`. -/
-structure ReflPrefunctor (V : Type u₁) [ReflQuiver.{v₁} V] (W : Type u₂) [ReflQuiver.{v₂} W]
-    extends Prefunctor V W where
-  /-- A functor preserves identity morphisms. -/
-  map_id : ∀ X : V, map (𝟙rq X) = 𝟙rq (obj X) := by aesop_cat
-
-namespace ReflPrefunctor
-
--- Porting note: added during port.
--- These lemmas can not be `@[simp]` because after `whnfR` they have a variable on the LHS.
--- Nevertheless they are sometimes useful when building functors.
-lemma mk_obj {V W : Type*} [ReflQuiver V] [ReflQuiver W] {obj : V → W} {map} {X : V} :
-    (Prefunctor.mk obj map).obj X = obj X := rfl
-
-lemma mk_map {V W : Type*} [ReflQuiver V] [ReflQuiver W] {obj : V → W} {map} {X Y : V} {f : X ⟶ Y} :
-    (Prefunctor.mk obj map).map f = map f := rfl
-
--- @[ext]
-theorem ext {V : Type u} [ReflQuiver.{v₁} V] {W : Type u₂} [ReflQuiver.{v₂} W] {F G : ReflPrefunctor V W}
-    (h_obj : ∀ X, F.obj X = G.obj X)
-    (h_map : ∀ (X Y : V) (f : X ⟶ Y),
-      F.map f = Eq.recOn (h_obj Y).symm (Eq.recOn (h_obj X).symm (G.map f))) : F = G := by
-  obtain ⟨⟨F_obj⟩⟩ := F
-  obtain ⟨⟨G_obj⟩⟩ := G
-  obtain rfl : F_obj = G_obj := (Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _
-  congr
-  funext X Y f
-  simpa using h_map X Y f
-
-/-- The identity morphism between quivers. -/
-@[simps!]
-def id (V : Type*) [ReflQuiver V] : ReflPrefunctor V V where
-  __ := Prefunctor.id _
-  map_id _ := rfl
-
-instance (V : Type*) [ReflQuiver V] : Inhabited (ReflPrefunctor V V) :=
-  ⟨id V⟩
-
-/-- Composition of morphisms between quivers. -/
-@[simps!]
-def comp {U : Type*} [ReflQuiver U] {V : Type*} [ReflQuiver V] {W : Type*} [ReflQuiver W]
-    (F : ReflPrefunctor U V) (G : ReflPrefunctor V W) : ReflPrefunctor U W where
-  __ := F.toPrefunctor.comp G.toPrefunctor
-  map_id _ := by simp [F.map_id, G.map_id]
-
-@[simp]
-theorem comp_id {U V : Type*} [ReflQuiver U] [ReflQuiver V] (F : ReflPrefunctor U V) :
-    F.comp (id _) = F := rfl
-
-@[simp]
-theorem id_comp {U V : Type*} [ReflQuiver U] [ReflQuiver V] (F : ReflPrefunctor U V) :
-    (id _).comp F = F := rfl
-
-@[simp]
-theorem comp_assoc {U V W Z : Type*} [ReflQuiver U] [ReflQuiver V] [ReflQuiver W] [ReflQuiver Z]
-    (F : ReflPrefunctor U V) (G : ReflPrefunctor V W) (H : ReflPrefunctor W Z) :
-    (F.comp G).comp H = F.comp (G.comp H) := rfl
-
-/-- Notation for a prefunctor between quivers. -/
-infixl:50 " ⥤rq " => ReflPrefunctor
-
-/-- Notation for composition of prefunctors. -/
-infixl:60 " ⋙rq " => ReflPrefunctor.comp
-
-/-- Notation for the identity prefunctor on a quiver. -/
-notation "𝟭rq" => id
-
-theorem congr_map {U V : Type*} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y}
-    (h : f = g) : F.map f = F.map g := congrArg F.map h
-
-end ReflPrefunctor
-
-def Functor.toReflPrefunctor {C D} [Category C] [Category D] (F : C ⥤ D) : C ⥤rq D := { F with }
-
-@[simp]
-theorem Functor.toReflPrefunctor_toPrefunctor {C D : Cat} (F : C ⥤ D) :
-    (Functor.toReflPrefunctor F).toPrefunctor = F.toPrefunctor := rfl
-
-namespace ReflQuiver
-open Opposite
-
-/-- `Vᵒᵖ` reverses the direction of all arrows of `V`. -/
-instance opposite {V} [ReflQuiver V] : ReflQuiver Vᵒᵖ where
-   id X := op (𝟙rq X.unop)
-
-instance discreteQuiver (V : Type u) : ReflQuiver.{u+1} (Discrete V) := { discreteCategory V with }
-
-end ReflQuiver
-
--- NB: Copied to ForMathlib/CategoryTheory/Category/ReflQuiv.lean
-@[nolint checkUnivs]
-def ReflQuiv :=
-  Bundled ReflQuiver.{v + 1, u}
-
-namespace ReflQuiv
-
-instance : CoeSort ReflQuiv (Type u) where coe := Bundled.α
-
-instance str' (C : ReflQuiv.{v, u}) : ReflQuiver.{v + 1, u} C := C.str
-
-def toQuiv (C : ReflQuiv.{v, u}) : Quiv.{v, u} := Quiv.of C.α
-
-/-- Construct a bundled `ReflQuiv` from the underlying type and the typeclass. -/
-def of (C : Type u) [ReflQuiver.{v + 1} C] : ReflQuiv.{v, u} := Bundled.of C
-
-instance : Inhabited ReflQuiv := ⟨ReflQuiv.of (Discrete default)⟩
-
-@[simp] theorem of_val (C : Type u) [ReflQuiver C] : (ReflQuiv.of C) = C := rfl
-
-/-- Category structure on `ReflQuiv` -/
-instance category : LargeCategory.{max v u} ReflQuiv.{v, u} where
-  Hom C D := ReflPrefunctor C D
-  id C := ReflPrefunctor.id C
-  comp F G := ReflPrefunctor.comp F G
-
-theorem id_eq_id (X : ReflQuiv) : 𝟙 X = 𝟭rq X := rfl
-theorem comp_eq_comp {X Y Z : ReflQuiv} (F : X ⟶ Y) (G : Y ⟶ Z) : F ≫ G = F ⋙rq G := rfl
-
-/-- The forgetful functor from categories to quivers. -/
-@[simps]
-def forget : Cat.{v, u} ⥤ ReflQuiv.{v, u} where
-  obj C := ReflQuiv.of C
-  map F := F.toReflPrefunctor
-
-theorem forget_faithful {C D : Cat.{v, u}} (F G : C ⥤ D)
-    (hyp : forget.map F = forget.map G) : F = G := by
-  cases F; cases G; cases hyp; rfl
-
-theorem forget.Faithful : Functor.Faithful (forget) where
-  map_injective := fun hyp ↦ forget_faithful _ _ hyp
-
-/-- The forgetful functor from categories to quivers. -/
-@[simps]
-def forgetToQuiv : ReflQuiv.{v, u} ⥤ Quiv.{v, u} where
-  obj V := Quiv.of V
-  map F := F.toPrefunctor
-
-theorem forgetToQuiv_faithful {V W : ReflQuiv} (F G : V ⥤rq W)
-    (hyp : forgetToQuiv.map F = forgetToQuiv.map G) : F = G := by
-  cases F; cases G; cases hyp; rfl
-
-theorem forgetToQuiv.Faithful : Functor.Faithful (forgetToQuiv) where
-  map_injective := fun hyp ↦ forgetToQuiv_faithful _ _ hyp
-
-theorem forget_forgetToQuiv : forget ⋙ forgetToQuiv = Quiv.forget := rfl
-
-end ReflQuiv
-
-namespace ReflPrefunctor
-
-def toFunctor {C D : Cat} (F : (ReflQuiv.of C) ⟶ (ReflQuiv.of D))
-    (hyp : ∀ {X Y Z : ↑C} (f : X ⟶ Y) (g : Y ⟶ Z),
-      F.map (CategoryStruct.comp (obj := C) f g) =
-        CategoryStruct.comp (obj := D) (F.map f) (F.map g)) : C ⥤ D where
-  obj := F.obj
-  map := F.map
-  map_id := F.map_id
-  map_comp := hyp
-
-end ReflPrefunctor
-namespace Cat
-
-inductive FreeReflRel {V} [ReflQuiver V] : (X Y : Paths V) → (f g : X ⟶ Y) → Prop
-  | mk {X : V} : FreeReflRel X X (Quiver.Hom.toPath (𝟙rq X)) .nil
-
-def FreeRefl (V) [ReflQuiver V] :=
-  Quotient (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V))
-
-instance (V) [ReflQuiver V] : Category (FreeRefl V) :=
-  inferInstanceAs (Category (Quotient _))
-
-def FreeRefl.quotientFunctor (V) [ReflQuiver V] : Cat.free.obj (Quiv.of V) ⥤ FreeRefl V :=
-  Quotient.functor (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V))
-
-theorem FreeRefl.lift_unique' {V} [ReflQuiver V] {D} [Category D] (F₁ F₂ : FreeRefl V ⥤ D)
-    (h : quotientFunctor V ⋙ F₁ = quotientFunctor V ⋙ F₂) :
-    F₁ = F₂ :=
-  Quotient.lift_unique' (C := Cat.free.obj (Quiv.of V)) (FreeReflRel (V := V)) _ _ h
-
-@[simps!]
-def freeRefl : ReflQuiv.{v, u} ⥤ Cat.{max u v, u} where
-  obj V := Cat.of (FreeRefl V)
-  map f := Quotient.lift _ ((by exact Cat.free.map f.toPrefunctor) ⋙ FreeRefl.quotientFunctor _)
-    (fun X Y f g hfg => by
-      apply Quotient.sound
-      cases hfg
-      simp [ReflPrefunctor.map_id]
-      constructor)
-  map_id X := by
-    dsimp
-    refine (Quotient.lift_unique _ _ _ _ ((Functor.comp_id _).trans <|
-      (Functor.id_comp _).symm.trans ?_)).symm
-    congr 1
-    exact (free.map_id X.toQuiv).symm
-  map_comp {X Y Z} f g := by
-    dsimp
-    apply (Quotient.lift_unique _ _ _ _ _).symm
-    have : free.map (f ≫ g).toPrefunctor =
-        free.map (X := X.toQuiv) (Y := Y.toQuiv) f.toPrefunctor ⋙
-        free.map (X := Y.toQuiv) (Y := Z.toQuiv) g.toPrefunctor := by
-      show _ = _ ≫ _
-      rw [← Functor.map_comp]; rfl
-    rw [this, Functor.assoc]
-    show _ ⋙ _ ⋙ _ = _
-    rw [← Functor.assoc, Quotient.lift_spec, Functor.assoc, FreeRefl.quotientFunctor,
-      Quotient.lift_spec]
-
-theorem freeRefl_naturality {X Y} [ReflQuiver X] [ReflQuiver Y] (f : X ⥤rq Y) :
-    free.map (X := Quiv.of X) (Y := Quiv.of Y) f.toPrefunctor ⋙
-    FreeRefl.quotientFunctor ↑Y =
-    FreeRefl.quotientFunctor ↑X ⋙ freeRefl.map (X := ReflQuiv.of X) (Y := ReflQuiv.of Y) f := by
-  simp only [free_obj, of_α, FreeRefl.quotientFunctor, freeRefl, ReflQuiv.of_val]
-  rw [Quotient.lift_spec]
-
-def freeReflNatTrans : ReflQuiv.forgetToQuiv ⋙ Cat.free ⟶ freeRefl where
-  app V := FreeRefl.quotientFunctor V
-  naturality _ _ f := freeRefl_naturality f
-
-end Cat
-
-namespace ReflQuiv
-
-@[simps! toPrefunctor obj map]
-def adj.unit.app (V : ReflQuiv.{max u v, u}) : V ⥤rq forget.obj (Cat.freeRefl.obj V) where
-  toPrefunctor := Quiv.adj.unit.app (V.toQuiv) ⋙q
-    Quiv.forget.map (Cat.FreeRefl.quotientFunctor V)
-  map_id := fun _ => Quotient.sound _ ⟨⟩
-
-/-- This is used in the proof of both triangle equalities. Should we simp?-/
-theorem adj.unit.component_eq (V : ReflQuiv.{max u v, u}) :
-    forgetToQuiv.map (adj.unit.app V) = Quiv.adj.unit.app (V.toQuiv) ≫
-    Quiv.forget.map (Y := Cat.of _) (Cat.FreeRefl.quotientFunctor V) := rfl
-
-@[simps!]
-def adj.counit.app (C : Cat) : Cat.freeRefl.obj (forget.obj C) ⥤ C := by
-  fapply Quotient.lift
-  · exact Quiv.adj.counit.app C
-  · intro x y f g rel
-    cases rel
-    unfold Quiv.adj
-    simp only [id_obj, forget_obj, Cat.free_obj, Quiv.forget_obj,
-      Adjunction.mkOfHomEquiv_counit_app, Equiv.invFun_as_coe, Equiv.coe_fn_symm_mk, Quiv.lift_obj,
-      ReflQuiver.id_eq_id, Quiv.lift_map, Prefunctor.mapPath_toPath, composePath_toPath,
-      Prefunctor.mapPath_nil, composePath_nil]
-    rfl
-
-/-- This is used in the proof of both triangle equalities. -/
-@[simp]
-theorem adj.counit.component_eq (C : Cat) :
-    Cat.FreeRefl.quotientFunctor C ⋙ adj.counit.app C =
-    Quiv.adj.counit.app C := rfl
-
-@[simp]
-theorem adj.counit.component_eq' (C) [Category C] :
-    Cat.FreeRefl.quotientFunctor C ⋙ adj.counit.app (Cat.of C) =
-    Quiv.adj.counit.app (Cat.of C) := rfl
-
-/--
-The adjunction between forming the free category on a quiver, and forgetting a category to a quiver.
--/
-nonrec def adj : Cat.freeRefl.{max u v, u} ⊣ ReflQuiv.forget :=
-  Adjunction.mkOfUnitCounit {
-    unit := {
-      app := adj.unit.app
-      naturality := fun V W f ↦ by exact rfl
-    }
-    counit := {
-      app := adj.counit.app
-      naturality := fun C D F ↦ Quotient.lift_unique' _ _ _ (Quiv.adj.counit.naturality F)
-    }
-    left_triangle := by
-      ext V
-      apply Cat.FreeRefl.lift_unique'
-      simp only [id_obj, Cat.free_obj, Cat.of_α, comp_obj, Cat.freeRefl_obj_α, NatTrans.comp_app,
-        forget_obj, whiskerRight_app, associator_hom_app, whiskerLeft_app, id_comp, NatTrans.id_app']
-      rw [Cat.id_eq_id, Cat.comp_eq_comp]
-      simp only [Cat.freeRefl_obj_α, Functor.comp_id]
-      rw [← Functor.assoc, ← Cat.freeRefl_naturality, Functor.assoc]
-      dsimp [Cat.freeRefl]
-      rw [adj.counit.component_eq' (Cat.FreeRefl V)]
-      conv =>
-        enter [1, 1, 2]
-        apply (Quiv.comp_eq_comp (X := Quiv.of _) (Y := Quiv.of _) (Z := Quiv.of _) ..).symm
-      rw [Cat.free.map_comp]
-      show (_ ⋙ ((Quiv.forget ⋙ Cat.free).map (X := Cat.of _) (Y := Cat.of _)
-        (Cat.FreeRefl.quotientFunctor V))) ⋙ _ = _
-      rw [Functor.assoc, ← Cat.comp_eq_comp]
-      conv => enter [1, 2]; apply Quiv.adj.counit.naturality
-      rw [Cat.comp_eq_comp, ← Functor.assoc, ← Cat.comp_eq_comp]
-      conv => enter [1, 1]; apply Quiv.adj.left_triangle_components V.toQuiv
-      exact Functor.id_comp _
-    right_triangle := by
-      ext C
-      simp only [comp_obj, forget_obj, id_obj, NatTrans.comp_app, Cat.freeRefl_obj_α, of_val,
-        whiskerLeft_app, associator_inv_app, whiskerRight_app, forget_map, id_comp,
-        NatTrans.id_app']
-      exact forgetToQuiv_faithful _ _ (Quiv.adj.right_triangle_components C)
-  }
-
-end ReflQuiv
-
 -- NB: Moved to Order.Category.NonEmptyFiniteLinOrd.lean; who knows if this is correct
 theorem Fin.le_succ {n} (i : Fin n) : i.castSucc ≤ i.succ := Nat.le_succ i
 
@@ -1617,7 +1291,7 @@ theorem oneTruncation₂_toNerve₂Mk' {X : SSet.Truncated 2} {C : Cat}
         ((f ≫ (forgetToReflQuiv.natIso.app C).hom).map (ev12₂ φ))) :
     oneTruncation₂.map (toNerve₂.mk' f hyp) = f := by
   refine ReflPrefunctor.ext (fun _ ↦ ComposableArrows.ext₀ rfl)
-    (fun X Y g ↦ eq_of_heq ((heq_eqRec_iff_heq _ _ _).2 <| (heq_eqRec_iff_heq _ _ _).2 ?_))
+    (fun X Y g ↦ eq_of_heq (heq_eqRec_iff_heq.2 <| heq_eqRec_iff_heq.2 ?_))
   simp [oneTruncation₂]
   have {A B A' B' : OneTruncation₂ (nerveFunctor₂.obj C)}
       : A = A' → B = B' → ∀ (x : A ⟶ B) (y : A' ⟶ B'), x.1 = y.1 → HEq x y := by

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e0b13c946e9c3805f1eec785c72955e103a9cbaf",
+   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
+   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2b108d1e9018455f2a4d06b17b06a0f689f42278",
+   "rev": "85e29307e7dd45b763f368e20254ae6d90b1a757",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,