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] : MorphismProperty (Functor J C)

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 α β)

instance CategoryTheory.NatTrans.instIsMultiplicativeFunctorEquifibered {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] : Equifibered.IsMultiplicative

instance CategoryTheory.NatTrans.instRespectsIsoFunctorEquifibered {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] : Equifibered.RespectsIso

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 α

def CategoryTheory.NatTrans.Coequifibered {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] : MorphismProperty (Functor J C)

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 α β)

instance CategoryTheory.NatTrans.instIsMultiplicativeFunctorCoequifibered {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] : Coequifibered.IsMultiplicative

instance CategoryTheory.NatTrans.instRespectsIsoFunctorCoequifibered {J : Type u_1} {C : Type u_3} [Category.{v_1, u_1} J] [Category.{v_2, u_3} C] : Coequifibered.RespectsIso

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 α)

theorem CategoryTheory.NatTrans.Equifibered.rightOp {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.rightOp α)

theorem CategoryTheory.NatTrans.Coequifibered.rightOp {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.rightOp α)

theorem CategoryTheory.NatTrans.coequifibered_op_iff {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} : Coequifibered (NatTrans.op α) ↔ Equifibered α

theorem CategoryTheory.NatTrans.equifibered_op_iff {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} : Equifibered (NatTrans.op α) ↔ Coequifibered α

theorem CategoryTheory.NatTrans.coequifibered_unop_iff {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} : Coequifibered (NatTrans.unop α) ↔ Equifibered α

theorem CategoryTheory.NatTrans.equifibered_unop_iff {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} : Equifibered (NatTrans.unop α) ↔ Coequifibered α