multiequalizerEquiv — Mathlib

English

A set of internal lemmas controlling how the auxiliary equivalence behaves on morphisms and coordinates.

Русский

Набор внутренних лемм, управляющих поведением вспомогательного эквивалентного отображения на морфизмах и координатах.

LaTeX

$$$\\text{Aux proofs for } multiequalizerEquivAux \\text{ describing map behavior on left/right coordinates.}$$$

Lean4

/-- The equivalence between the noncomputable multiequalizer and
the concrete multiequalizer. -/
noncomputable def multiequalizerEquiv {J : MulticospanShape.{w, w'}} (I : MulticospanIndex J C) [HasMultiequalizer I]
    [PreservesLimit I.multicospan (forget C)] :
    ToType (multiequalizer I) ≃ { x : ∀ i : J.L, ToType (I.left i) // ∀ i : J.R, I.fst i (x _) = I.snd i (x _) } :=
  letI h1 := limit.isLimit I.multicospan
  letI h2 := isLimitOfPreserves (forget C) h1
  (Types.isLimitEquivSections h2).trans (Concrete.multiequalizerEquivAux I)

Похожие утверждения