equiv_symm_eq_apply — Mathlib

English

There is a natural equivalence between the type associated to the multiequalizer and Meq P S.

Русский

Существует естественное тождество между типом, связанным с мультинeквaлeйзером, и Meq P S.

LaTeX

$$$\text{Meq.equiv}: ToType(\text{multiequalizer}(S.index P)) \simeq Meq P S$$$

Lean4

theorem equiv_symm_eq_apply {X : C} {P : Cᵒᵖ ⥤ D} {S : J.Cover X} [HasMultiequalizer (S.index P)] (x : Meq P S)
    (I : S.Arrow) :
    -- We can hint `ConcreteCategory.hom (Y := P.obj (op I.Y))` below to put it into `simp`-normal
        -- form, but that doesn't seem to fix the `erw`s below...
    (Multiequalizer.ι (S.index P) I) ((Meq.equiv P S).symm x) = x I := by
  simp [← GrothendieckTopology.Cover.index_left, ← equiv_apply]

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