discreteEquiv — Mathlib

English

The equivalence Arrow(Discrete S) ≃ S has toFun given by taking the source object and invFun sending s ↦ Arrow.mk (Id_{Discrete s}); left_inv holds.

Русский

Эквивалентность Arrow(Discrete S) ≃ S имеет отображение toFun, выдающее исходную сущность стрелы, и обратное invFun, отправляющее s в стрелу с тождественным отображением, левые инверсии выполняются.

LaTeX

$$$Arrow(Discrete(S)) \simeq S$$$

Lean4

/-- The equivalence `Arrow (Discrete S) ≃ S`. -/
def discreteEquiv (S : Type u) : Arrow (Discrete S) ≃ S
    where
  toFun f := f.left.as
  invFun s := Arrow.mk (𝟙 (Discrete.mk s))
  left_inv := by
    rintro ⟨⟨_⟩, ⟨_⟩, f⟩
    obtain rfl := Discrete.eq_of_hom f
    rfl

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