Equifibered natural transformation

Main definition

• CategoryTheory.NatTrans.Equifibered: A natural transformation α : F ⟶ G is equifibered if every commutative square of the following form is a pullback.

F(X) → F(Y)
 ↓      ↓
G(X) → G(Y)

• CategoryTheory.NatTrans.Coequifibered: The dual notion.

def CategoryTheory.NatTrans.Equifibered {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor J C} (α : F ⟶ G) : Prop

A natural transformation is equifibered if every commutative square of the following form is a pullback.

F(X) → F(Y)
 ↓      ↓
G(X) → G(Y)

Equations

• CategoryTheory.NatTrans.Equifibered α = ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.IsPullback (F.map f) (α.app i) (α.app j) (G.map f)

theorem CategoryTheory.NatTrans.equifibered_of_isIso {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor J C} (α : F ⟶ G) [IsIso α] : Equifibered α

theorem CategoryTheory.NatTrans.Equifibered.comp {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G H : Functor J C} {α : F ⟶ G} {β : G ⟶ H} (hα : Equifibered α) (hβ : Equifibered β) : Equifibered (CategoryStruct.comp α β)

theorem CategoryTheory.NatTrans.Equifibered.whiskerRight {J : Type u_1} {C : Type u_3} {D : Type u_4} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] [Category.{v_4, u_4} D] {F G : Functor J C} {α : F ⟶ G} (hα : Equifibered α) (H : Functor C D) [∀ (i j : J) (f : j ⟶ i), Limits.PreservesLimit (Limits.cospan (α.app i) (G.map f)) H] : Equifibered (Functor.whiskerRight α H)

theorem CategoryTheory.NatTrans.Equifibered.whiskerLeft {J : Type u_1} {K : Type u_2} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] [Category.{v_3, u_2} K] {F G : Functor J C} {α : F ⟶ G} (hα : Equifibered α) (H : Functor K J) : Equifibered (H.whiskerLeft α)

theorem CategoryTheory.NatTrans.Equifibered.of_discrete {C : Type u_3} {ι : Type u_5} [Category.{v_2, u_3} C] {F G : Functor (Discrete ι) C} (α : F ⟶ G) : Equifibered α

@[deprecated CategoryTheory.NatTrans.Equifibered.of_discrete (since := "2026-01-23")]

theorem CategoryTheory.mapPair_equifibered {C : Type u_3} {ι : Type u_5} [Category.{v_2, u_3} C] {F G : Functor (Discrete ι) C} (α : F ⟶ G) : NatTrans.Equifibered α

Alias of CategoryTheory.NatTrans.Equifibered.of_discrete.

@[deprecated CategoryTheory.NatTrans.Equifibered.of_discrete (since := "2026-01-23")]

theorem CategoryTheory.NatTrans.equifibered_of_discrete {C : Type u_3} {ι : Type u_5} [Category.{v_2, u_3} C] {F G : Functor (Discrete ι) C} (α : F ⟶ G) : Equifibered α

Alias of CategoryTheory.NatTrans.Equifibered.of_discrete.

def CategoryTheory.NatTrans.Coequifibered {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor J C} (α : F ⟶ G) : Prop

A natural transformation is co-equifibered if every commutative square of the following form is a pushout.

F(X) → F(Y)
 ↓      ↓
G(X) → G(Y)

Equations

• CategoryTheory.NatTrans.Coequifibered α = ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.IsPushout (F.map f) (α.app i) (α.app j) (G.map f)

theorem CategoryTheory.NatTrans.Coequifibered_of_isIso {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor J C} (α : F ⟶ G) [IsIso α] : Coequifibered α

theorem CategoryTheory.NatTrans.Coequifibered.comp {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G H : Functor J C} {α : F ⟶ G} {β : G ⟶ H} (hα : Coequifibered α) (hβ : Coequifibered β) : Coequifibered (CategoryStruct.comp α β)

theorem CategoryTheory.NatTrans.Coequifibered.whiskerRight {J : Type u_1} {C : Type u_3} {D : Type u_4} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] [Category.{v_4, u_4} D] {F G : Functor J C} {α : F ⟶ G} (hα : Coequifibered α) (H : Functor C D) [∀ (i j : J) (f : j ⟶ i), Limits.PreservesColimit (Limits.span (F.map f) (α.app j)) H] : Coequifibered (Functor.whiskerRight α H)

theorem CategoryTheory.NatTrans.Coequifibered.whiskerLeft {J : Type u_1} {K : Type u_2} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] [Category.{v_3, u_2} K] {F G : Functor J C} {α : F ⟶ G} (hα : Coequifibered α) (H : Functor K J) : Coequifibered (H.whiskerLeft α)

theorem CategoryTheory.NatTrans.Coequifibered.of_discrete {C : Type u_3} [Category.{v_2, u_3} C] {ι : Type u_6} {F G : Functor (Discrete ι) C} (α : F ⟶ G) : Equifibered α

theorem CategoryTheory.NatTrans.Coequifibered.op {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor J C} {α : F ⟶ G} (hα : Coequifibered α) : Equifibered (NatTrans.op α)

theorem CategoryTheory.NatTrans.Equifibered.op {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor J C} {α : F ⟶ G} (hα : Equifibered α) : Coequifibered (NatTrans.op α)

theorem CategoryTheory.NatTrans.Coequifibered.unop {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor Jᵒᵖ Cᵒᵖ} {α : F ⟶ G} (hα : Coequifibered α) : Equifibered (NatTrans.unop α)

theorem CategoryTheory.NatTrans.Equifibered.unop {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] {F G : Functor Jᵒᵖ Cᵒᵖ} {α : F ⟶ G} (hα : Equifibered α) : Coequifibered (NatTrans.unop α)