feat: API for multiequalizers in the category of types (#14340)

In this PR, we give a concrete characterization of limit multiforks in the category of types.

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Author: joelriou

Mathlib/CategoryTheory/Limits/Shapes/Types.lean

@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Limits.Types
 import Mathlib.CategoryTheory.Limits.Shapes.Products
 import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
 import Mathlib.CategoryTheory.ConcreteCategory.Basic
 import Mathlib.Tactic.CategoryTheory.Elementwise
 import Mathlib.Data.Set.Subsingleton
@@ -31,6 +32,7 @@ giving the expected definitional implementation:
 * the coequalizer of a pair of maps `(f, g)` is the quotient of `Y` by `∀ x : Y, f x ~ g x`
 * the pullback of `f : X ⟶ Z` and `g : Y ⟶ Z` is the subtype `{ p : X × Y // f p.1 = g p.2 }`
   of the product
+* multiequalizers
 
 We first construct terms of `IsLimit` and `LimitCone`, and then provide isomorphisms with the
 types generated by the `HasLimit` API.
@@ -929,4 +931,86 @@ lemma pushoutCocone_inl_eq_inr_iff_of_isColimit {c : PushoutCocone f g} (hc : Is
 
 end Pushout
 
-end CategoryTheory.Limits.Types
+end Types
+
+section Multiequalizer
+
+variable (I : MulticospanIndex (Type u))
+
+/-- Given `I : MulticospanIndex (Type u)`, this is a type which identifies
+to the sections of the functor `I.multicospan`. -/
+@[ext]
+structure MulticospanIndex.sections where
+  /-- The data of an element in `I.left i` for each `i : I.L`. -/
+  val (i : I.L) : I.left i
+  property (r : I.R) : I.fst r (val _) = I.snd r (val _)
+
+/-- The bijection `I.sections ≃ I.multicospan.sections` when `I : MulticospanIndex (Type u)`
+is a multiequalizer diagram in the category of types. -/
+@[simps]
+def MulticospanIndex.sectionsEquiv :
+    I.sections ≃ I.multicospan.sections where
+  toFun s :=
+    { val := fun i ↦ match i with
+        | .left i => s.val i
+        | .right j => I.fst j (s.val _)
+      property := by
+        rintro _ _ (_|_|r)
+        · rfl
+        · rfl
+        · exact (s.property r).symm }
+  invFun s :=
+    { val := fun i ↦ s.val (.left i)
+      property := fun r ↦ (s.property (.fst r)).trans (s.property (.snd r)).symm }
+  left_inv _ := rfl
+  right_inv s := by
+    ext (_|r)
+    · rfl
+    · exact s.property (.fst r)
+
+namespace Multifork
+
+variable {I}
+variable (c : Multifork I)
+
+/-- Given a multiequalizer diagram `I : MulticospanIndex (Type u)` in the category of
+types and `c` a multifork for `I`, this is the canonical map `c.pt → I.sections`. -/
+@[simps]
+def toSections (x : c.pt) : I.sections where
+  val i := c.ι i x
+  property r := congr_fun (c.condition r) x
+
+lemma toSections_fac : I.sectionsEquiv.symm ∘ Types.sectionOfCone c = c.toSections := rfl
+
+/-- A multifork `c : Multifork I` in the category of types is limit iff the
+map `c.toSections : c.pt → I.sections` is a bijection. -/
+lemma isLimit_types_iff : Nonempty (IsLimit c) ↔ Function.Bijective c.toSections := by
+  rw [Types.isLimit_iff_bijective_sectionOfCone, ← toSections_fac, EquivLike.comp_bijective]
+
+namespace IsLimit
+
+variable {c}
+variable (hc : IsLimit c)
+
+/-- The bijection `I.sections ≃ c.pt` when `c : Multifork I` is a limit multifork
+in the category of types. -/
+noncomputable def sectionsEquiv : I.sections ≃ c.pt :=
+  (Equiv.ofBijective _ (c.isLimit_types_iff.1 ⟨hc⟩)).symm
+
+@[simp]
+lemma sectionsEquiv_symm_apply_val (x : c.pt) (i : I.L) :
+    ((sectionsEquiv hc).symm x).val i = c.ι i x := rfl
+
+@[simp]
+lemma sectionsEquiv_apply_val (s : I.sections) (i : I.L) :
+    c.ι i (sectionsEquiv hc s) = s.val i := by
+  obtain ⟨x, rfl⟩ := (sectionsEquiv hc).symm.surjective s
+  simp
+
+end IsLimit
+
+end Multifork
+
+end Multiequalizer
+
+end CategoryTheory.Limits