feat(CategoryTheory/Groupoid): various induction principles for morphisms (#42527)

Author: joelriou

Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean

@@ -348,6 +348,24 @@ lemma morphismProperty_eq_top {W : MorphismProperty V.HomotopyCategory}
     rintro _ _ _ ⟨_, _, e⟩
     exact hW e)
 
+/-- Induction principle for proving a property for all the morphisms
+in the homotopy category of a `2`-truncated simplicial set: it suffices
+to show that the property holds for morphisms induced by edges and that
+the property is stable under composition. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
+lemma hom_rec {motive : ∀ {x y : V.HomotopyCategory}, (x ⟶ y) → Prop}
+    (homMk : ∀ {x y : V _⦋0⦌₂} (e : Edge x y), motive (homMk e))
+    (comp : ∀ {x y z : V.HomotopyCategory} (f : x ⟶ y) (g : y ⟶ z),
+      motive f → motive g → motive (f ≫ g))
+    {x y : V.HomotopyCategory} (f : x ⟶ y) : motive f := by
+  let W : MorphismProperty V.HomotopyCategory := fun _ _ f ↦ motive f
+  have : W.IsMultiplicative :=
+    { id_mem x := by
+        obtain ⟨x, rfl⟩ := x.mk_surjective
+        simpa using! homMk (.id x)
+      comp_mem := comp }
+  exact (morphismProperty_eq_top (W := W) homMk).symm.le f (by simp)
+
 section
 
 variable {D : Type*} [Category* D]

Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean

@@ -139,6 +139,32 @@ theorem of_eq :
     of V = (Quiver.Symmetrify.of ⋙q (Paths.of (Quiver.Symmetrify V))).comp
       (Quotient.functor <| @redStep V _).toPrefunctor := rfl
 
+/-- Induction principle for proving a property for all the morphisms
+in the free groupoid of a quiver `V`: it suffices to prove the property
+for morphisms `(of V).map f` coming for the quiver `V` and their
+inverses, and that the property is multiplicative (i.e. stable under
+composition and satisfied by identities). -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
+lemma hom_rec {motive : ∀ {x y : Quiver.FreeGroupoid V}, (x ⟶ y) → Prop}
+    (of_map : ∀ {x y : V} (f : x ⟶ y), motive ((of V).map f))
+    (inv_of_map : ∀ {x y : V} (f : x ⟶ y), motive (inv ((of V).map f)))
+    (id : ∀ (x : V), motive (𝟙 ((of V).obj x)))
+    (comp : ∀ {x y z : Quiver.FreeGroupoid V} (f : x ⟶ y) (g : y ⟶ z),
+      motive f → motive g → motive (f ≫ g))
+    {x y : Quiver.FreeGroupoid V} (f : x ⟶ y) :
+    motive f := by
+  have {x y : Symmetrify V} (f : x ⟶ y) :
+      motive ((Quotient.functor _).map ((Paths.of _).map f)) := by
+    induction f with
+    | inl f => apply of_map
+    | inr f => simpa only [← Groupoid.inv_eq_inv] using! inv_of_map f
+  induction x with | _ x
+  induction y with | _ y
+  obtain ⟨f, rfl⟩ := (Quotient.functor _).map_surjective f
+  induction f using Paths.induction with
+  | id => apply id
+  | comp p f hp => simpa using! comp _ _ hp (this f)
+
 section UniversalProperty
 
 variable {V' : Type u'} [Groupoid V']

Mathlib/CategoryTheory/Groupoid/FreeGroupoidOfCategory.lean

@@ -93,6 +93,27 @@ lemma of_obj_bijective : Function.Bijective (of C).obj where
   left _ _ h := by cases h; rfl
   right X := ⟨X.as.as, rfl⟩
 
+/-- Induction principle for proving a property for all the morphisms
+in the free groupoid of a category `C`: it suffices to prove the property
+for morphisms coming from the category `C`, and that the property is
+stable under inverses and composition. -/
+@[elab_as_elim, cases_eliminator, induction_eliminator]
+lemma hom_rec {motive : ∀ ⦃x y : FreeGroupoid C⦄ (_ : x ⟶ y), Prop}
+    (homMk : ∀ ⦃x y : C⦄ (f : x ⟶ y), motive (homMk f))
+    (inv : ∀ ⦃x y : FreeGroupoid C⦄ (f : x ⟶ y), motive f → motive (inv f))
+    (comp : ∀ ⦃x y z : FreeGroupoid C⦄ (f : x ⟶ y) (g : y ⟶ z),
+      motive f → motive g → motive (f ≫ g))
+    {x y : FreeGroupoid C} (f : x ⟶ y) :
+    motive f := by
+  induction x with | _ x
+  induction y with | _ y
+  obtain ⟨f, rfl⟩ := (Quotient.functor (FreeGroupoid.homRel C)).map_surjective f
+  induction f with
+  | of_map f => exact homMk f
+  | inv_of_map f => simpa using! inv _ (homMk f)
+  | id x => simpa using! homMk (𝟙 x)
+  | comp _ _ hf hg => simpa using! comp _ _ hf hg
+
 section UniversalProperty
 
 variable {G : Type u₁} [Groupoid.{v₁} G]
@@ -132,6 +153,11 @@ theorem lift_unique (φ : C ⥤ G) (Φ : FreeGroupoid C ⥤ G) (hΦ : of C ⋙ 
   apply Quiver.FreeGroupoid.lift_unique
   exact congr_arg Functor.toPrefunctor hΦ
 
+lemma lift_unique' {Φ Φ' : FreeGroupoid C ⥤ G} (h : of C ⋙ Φ = of C ⋙ Φ') : Φ = Φ' := by
+  trans lift (of C ⋙ Φ')
+  · exact lift_unique _ _ h
+  · exact (lift_unique _ _ rfl).symm
+
 theorem lift_id_comp_of : lift (𝟭 G) ⋙ of G = 𝟭 _ := by
   rw [lift_unique (of G) (lift (𝟭 G) ⋙ of G) (by rw [← Functor.assoc, lift_spec, Functor.id_comp])]
   symm; apply lift_unique