equifibered_of_discrete — Mathlib

English

Let ι be any type and F, G: Discrete ι → C be two diagrams in a category C. Then any natural transformation α: F ⇒ G is equifibered (the equifibered condition holds automatically for discrete indexing).

Русский

Пусть ι — произвольный тип, и F, G: Discrete ι → C — диаграммы в категории C. Тогда любая натуральная трансформация α: F ⇒ G является эквифиберендной (условие эквифиберенности выполняется автоматически для дискретной индексации).

LaTeX

$$$\\operatorname{Equifibered}(\\alpha)$$$

Lean4

theorem equifibered_of_discrete {ι : Type*} {F G : Discrete ι ⥤ C} (α : F ⟶ G) : NatTrans.Equifibered α :=
  by
  rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
  simp only [Discrete.functor_map_id]
  exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩

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