pullbackId — Mathlib

English

Pulling back along identity is isomorphic to the identity functor on covers.

Русский

Вытягивание вдоль тождественного отображения изоморфно тождественному функтору на покрытиях.

LaTeX

$$$\mathrm{pullbackId}(X): J.pullback(\mathrm{id}_X) \cong \mathrm{Id}_{J.Cover(X)}$$$

Lean4

/-- Pulling back along the identity is naturally isomorphic to the identity functor. -/
def pullbackId (X : C) : J.pullback (𝟙 X) ≅ 𝟭 _ :=
  NatIso.ofComponents fun S => S.pullbackId

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