ι_desc — Mathlib

English

For any j ∈ J and x ∈ F.obj j, the descent along the cocone and the injection correspond: Quot.desc F c (Quot.ι F j x) = c.ι.app j x.

Русский

Пусть для каждого j ∈ J и x ∈ F.obj j выполнено: Quot.desc F c (Quot.ι F j x) = c.ι.app j x.

LaTeX

$$$ \mathrm{Quot}.\mathrm{desc} F c (\mathrm{Quot}.\mathrm{ι} F j x) = c.\mathrm{ι}.app j\, x $$$

Lean4

@[simp]
theorem ι_desc [DecidableEq J] (j : J) (x : F.obj j) : Quot.desc F c (Quot.ι F j x) = c.ι.app j x :=
  by
  dsimp [desc, ι]
  erw [QuotientAddGroup.lift_mk']
  simp

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