equifibered_of_isIso — Mathlib

English

If α: F ⟶ G is a natural transformation and α is an isomorphism (componentwise), then α is equifibered.

Русский

Если α: F ⟶ G — естественное преобразование и его компоненты образуют изоморфизм, то α является равнолистовым (equifibered).

LaTeX

$$IsIso α ⇒ Equifibered α$$

Lean4

theorem equifibered_of_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] : Equifibered α := fun _ _ f =>
  IsPullback.of_vert_isIso ⟨NatTrans.naturality _ f⟩

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