mapPair_equifibered — Mathlib

English

For functors F,F' : Discrete WalkingPair ⥤ C and α: F ⟶ F', α is equifibered.

Русский

Для категорий F,F': Discrete WalkingPair ⥤ C и естественного преобразования α: F ⟶ F', преобразование α равно равнолистово.

LaTeX

$$NatTrans.Equifibered α$$

Lean4

theorem mapPair_equifibered {F F' : Discrete WalkingPair ⥤ C} (α : F ⟶ F') : NatTrans.Equifibered α :=
  by
  rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩
  all_goals
    dsimp; simp only [Discrete.functor_map_id]
    exact IsPullback.of_horiz_isIso ⟨by simp only [Category.comp_id, Category.id_comp]⟩

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