Bundled exact functors #

We say that a functor F is left exact if it preserves finite limits, it is right exact if it preserves finite colimits, and it is exact if it is both left exact and right exact.

In this file, we define the categories of bundled left exact, right exact and exact functors.

source

def CategoryTheory.LeftExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Type (max (max (max u₁ u₂) v₁) v₂)

Bundled left-exact functors.

Equations

(C ⥤ₗ D) = CategoryTheory.ObjectProperty.FullSubcategory fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteLimits F

source

instance CategoryTheory.instCategoryLeftExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (C ⥤ₗ D)

Equations

CategoryTheory.instCategoryLeftExactFunctor C D = CategoryTheory.ObjectProperty.FullSubcategory.category fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteLimits F

source

def CategoryTheory.«term_⥤ₗ_» :

Lean.TrailingParserDescr

C ⥤ₗ D denotes left exact functors C ⥤ D

Equations

CategoryTheory.«term_⥤ₗ_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_⥤ₗ_» 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ₗ ") (Lean.ParserDescr.cat `term 26))

source

def CategoryTheory.LeftExactFunctor.forget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Functor (C ⥤ₗ D) (Functor C D)

A left exact functor is in particular a functor.

Equations

CategoryTheory.LeftExactFunctor.forget C D = CategoryTheory.ObjectProperty.ι fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteLimits F

source

instance CategoryTheory.instFullLeftExactFunctorFunctorForget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(LeftExactFunctor.forget C D).Full

source

instance CategoryTheory.instFaithfulLeftExactFunctorFunctorForget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(LeftExactFunctor.forget C D).Faithful

source

@[reducible, inline]

abbrev CategoryTheory.LeftExactFunctor.fullyFaithful (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(forget C D).FullyFaithful

The inclusion of left exact functors into functors is fully faithful.

Equations

CategoryTheory.LeftExactFunctor.fullyFaithful C D = CategoryTheory.ObjectProperty.fullyFaithfulι fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteLimits F

source

def CategoryTheory.RightExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Type (max (max (max u₁ u₂) v₁) v₂)

Bundled right-exact functors.

Equations

(C ⥤ᵣ D) = CategoryTheory.ObjectProperty.FullSubcategory fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteColimits F

source

instance CategoryTheory.instCategoryRightExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (C ⥤ᵣ D)

Equations

CategoryTheory.instCategoryRightExactFunctor C D = CategoryTheory.ObjectProperty.FullSubcategory.category fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteColimits F

source

def CategoryTheory.«term_⥤ᵣ_» :

Lean.TrailingParserDescr

C ⥤ᵣ D denotes right exact functors C ⥤ D

Equations

CategoryTheory.«term_⥤ᵣ_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_⥤ᵣ_» 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ᵣ ") (Lean.ParserDescr.cat `term 26))

source

def CategoryTheory.RightExactFunctor.forget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Functor (C ⥤ᵣ D) (Functor C D)

A right exact functor is in particular a functor.

Equations

CategoryTheory.RightExactFunctor.forget C D = CategoryTheory.ObjectProperty.ι fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteColimits F

source

instance CategoryTheory.instFullRightExactFunctorFunctorForget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(RightExactFunctor.forget C D).Full

source

instance CategoryTheory.instFaithfulRightExactFunctorFunctorForget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(RightExactFunctor.forget C D).Faithful

source

@[reducible, inline]

abbrev CategoryTheory.RightExactFunctor.fullyFaithful (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(forget C D).FullyFaithful

The inclusion of right exact functors into functors is fully faithful.

Equations

CategoryTheory.RightExactFunctor.fullyFaithful C D = CategoryTheory.ObjectProperty.fullyFaithfulι fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteColimits F

source

def CategoryTheory.ExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Type (max (max (max u₁ u₂) v₁) v₂)

Bundled exact functors.

Equations

(C ⥤ₑ D) = CategoryTheory.ObjectProperty.FullSubcategory fun (F : CategoryTheory.Functor C D) => CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F

source

instance CategoryTheory.instCategoryExactFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (C ⥤ₑ D)

Equations

One or more equations did not get rendered due to their size.

source

def CategoryTheory.«term_⥤ₑ_» :

Lean.TrailingParserDescr

C ⥤ₑ D denotes exact functors C ⥤ D

Equations

CategoryTheory.«term_⥤ₑ_» = Lean.ParserDescr.trailingNode `CategoryTheory.«term_⥤ₑ_» 26 27 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤ₑ ") (Lean.ParserDescr.cat `term 26))

source

def CategoryTheory.ExactFunctor.forget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Functor (C ⥤ₑ D) (Functor C D)

An exact functor is in particular a functor.

Equations

One or more equations did not get rendered due to their size.

source

instance CategoryTheory.instFullExactFunctorFunctorForget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(ExactFunctor.forget C D).Full

source

instance CategoryTheory.instFaithfulExactFunctorFunctorForget (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(ExactFunctor.forget C D).Faithful

source

def CategoryTheory.LeftExactFunctor.ofExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Functor (C ⥤ₑ D) (C ⥤ₗ D)

Turn an exact functor into a left exact functor.

Equations

CategoryTheory.LeftExactFunctor.ofExact C D = CategoryTheory.ObjectProperty.ιOfLE ⋯

source

instance CategoryTheory.instFullExactFunctorLeftExactFunctorOfExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(LeftExactFunctor.ofExact C D).Full

source

instance CategoryTheory.instFaithfulExactFunctorLeftExactFunctorOfExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(LeftExactFunctor.ofExact C D).Faithful

source

def CategoryTheory.RightExactFunctor.ofExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Functor (C ⥤ₑ D) (C ⥤ᵣ D)

Turn an exact functor into a left exact functor.

Equations

CategoryTheory.RightExactFunctor.ofExact C D = CategoryTheory.ObjectProperty.ιOfLE ⋯

source

instance CategoryTheory.instFullExactFunctorRightExactFunctorOfExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(RightExactFunctor.ofExact C D).Full

source

instance CategoryTheory.instFaithfulExactFunctorRightExactFunctorOfExact (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

(RightExactFunctor.ofExact C D).Faithful

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.ofExact_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) :

(ofExact C D).obj F = { obj := F.obj, property := ⋯ }

source

@[simp]

theorem CategoryTheory.RightExactFunctor.ofExact_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) :

(ofExact C D).obj F = { obj := F.obj, property := ⋯ }

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.ofExact_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) :

(ofExact C D).map α = α

source

@[simp]

theorem CategoryTheory.RightExactFunctor.ofExact_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) :

(ofExact C D).map α = α

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₗ D) :

(forget C D).obj F = F.obj

source

@[simp]

theorem CategoryTheory.RightExactFunctor.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ᵣ D) :

(forget C D).obj F = F.obj

source

@[simp]

theorem CategoryTheory.ExactFunctor.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) :

(forget C D).obj F = F.obj

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.forget_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₗ D} (α : F ⟶ G) :

(forget C D).map α = α

source

@[simp]

theorem CategoryTheory.RightExactFunctor.forget_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ᵣ D} (α : F ⟶ G) :

(forget C D).map α = α

source

@[simp]

theorem CategoryTheory.ExactFunctor.forget_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : C ⥤ₑ D} (α : F ⟶ G) :

(forget C D).map α = α

source

def CategoryTheory.LeftExactFunctor.of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] :

C ⥤ₗ D

Turn a left exact functor into an object of the category LeftExactFunctor C D.

Equations

CategoryTheory.LeftExactFunctor.of F = { obj := F, property := ⋯ }

source

def CategoryTheory.RightExactFunctor.of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteColimits F] :

C ⥤ᵣ D

Turn a right exact functor into an object of the category RightExactFunctor C D.

Equations

CategoryTheory.RightExactFunctor.of F = { obj := F, property := ⋯ }

source

def CategoryTheory.ExactFunctor.of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] :

C ⥤ₑ D

Turn an exact functor into an object of the category ExactFunctor C D.

Equations

CategoryTheory.ExactFunctor.of F = { obj := F, property := ⋯ }

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.of_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] :

(of F).obj = F

source

@[simp]

theorem CategoryTheory.RightExactFunctor.of_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteColimits F] :

(of F).obj = F

source

@[simp]

theorem CategoryTheory.ExactFunctor.of_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] :

(of F).obj = F

source

theorem CategoryTheory.LeftExactFunctor.forget_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] :

(forget C D).obj (of F) = F

source

theorem CategoryTheory.RightExactFunctor.forget_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteColimits F] :

(forget C D).obj (of F) = F

source

theorem CategoryTheory.ExactFunctor.forget_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] :

(forget C D).obj (of F) = F

source

instance CategoryTheory.instPreservesFiniteLimitsObjFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₗ D) :

Limits.PreservesFiniteLimits F.obj

source

instance CategoryTheory.instPreservesFiniteColimitsObjFunctor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ᵣ D) :

Limits.PreservesFiniteColimits F.obj

source

instance CategoryTheory.instPreservesFiniteLimitsObjFunctorAndPreservesFiniteColimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) :

Limits.PreservesFiniteLimits F.obj

source

instance CategoryTheory.instPreservesFiniteColimitsObjFunctorAndPreservesFiniteLimits {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : C ⥤ₑ D) :

Limits.PreservesFiniteColimits F.obj

source

def CategoryTheory.LeftExactFunctor.whiskeringLeft (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :

Functor (C ⥤ₗ D) (Functor (D ⥤ₗ E) (C ⥤ₗ E))

Whiskering a left exact functor by a left exact functor yields a left exact functor.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₗ D) (X : D ⥤ₗ E) :

((whiskeringLeft C D E).obj F).obj X = { obj := F.obj.comp X.obj, property := ⋯ }

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : C ⥤ₗ D} (η : F ⟶ G) (H : D ⥤ₗ E) (c : C) :

(((whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringLeft_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₗ D) {X✝ Y✝ : D ⥤ₗ E} (f : X✝ ⟶ Y✝) :

((whiskeringLeft C D E).obj F).map f = whiskerLeft F.obj f

source

def CategoryTheory.LeftExactFunctor.whiskeringRight (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :

Functor (D ⥤ₗ E) (Functor (C ⥤ₗ D) (C ⥤ₗ E))

Whiskering a left exact functor by a left exact functor yields a left exact functor.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : D ⥤ₗ E} (η : F ⟶ G) (H : C ⥤ₗ D) (c : C) :

(((whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₗ E) {X✝ Y✝ : C ⥤ₗ D} (f : X✝ ⟶ Y✝) :

((whiskeringRight C D E).obj F).map f = whiskerRight f F.obj

source

@[simp]

theorem CategoryTheory.LeftExactFunctor.whiskeringRight_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₗ E) (X : C ⥤ₗ D) :

((whiskeringRight C D E).obj F).obj X = { obj := X.obj.comp F.obj, property := ⋯ }

source

def CategoryTheory.RightExactFunctor.whiskeringLeft (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :

Functor (C ⥤ᵣ D) (Functor (D ⥤ᵣ E) (C ⥤ᵣ E))

Whiskering a right exact functor by a right exact functor yields a right exact functor.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ᵣ D) {X✝ Y✝ : D ⥤ᵣ E} (f : X✝ ⟶ Y✝) :

((whiskeringLeft C D E).obj F).map f = whiskerLeft F.obj f

source

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ᵣ D) (X : D ⥤ᵣ E) :

((whiskeringLeft C D E).obj F).obj X = { obj := F.obj.comp X.obj, property := ⋯ }

source

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringLeft_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : C ⥤ᵣ D} (η : F ⟶ G) (H : D ⥤ᵣ E) (c : C) :

(((whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

source

def CategoryTheory.RightExactFunctor.whiskeringRight (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :

Functor (D ⥤ᵣ E) (Functor (C ⥤ᵣ D) (C ⥤ᵣ E))

Whiskering a right exact functor by a right exact functor yields a right exact functor.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ᵣ E) {X✝ Y✝ : C ⥤ᵣ D} (f : X✝ ⟶ Y✝) :

((whiskeringRight C D E).obj F).map f = whiskerRight f F.obj

source

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ᵣ E) (X : C ⥤ᵣ D) :

((whiskeringRight C D E).obj F).obj X = { obj := X.obj.comp F.obj, property := ⋯ }

source

@[simp]

theorem CategoryTheory.RightExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : D ⥤ᵣ E} (η : F ⟶ G) (H : C ⥤ᵣ D) (c : C) :

(((whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)

source

def CategoryTheory.ExactFunctor.whiskeringLeft (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :

Functor (C ⥤ₑ D) (Functor (D ⥤ₑ E) (C ⥤ₑ E))

Whiskering an exact functor by an exact functor yields an exact functor.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₑ D) {X✝ Y✝ : D ⥤ₑ E} (f : X✝ ⟶ Y✝) :

((whiskeringLeft C D E).obj F).map f = whiskerLeft F.obj f

source

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : C ⥤ₑ D) (X : D ⥤ₑ E) :

((whiskeringLeft C D E).obj F).obj X = { obj := F.obj.comp X.obj, property := ⋯ }

source

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringLeft_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : C ⥤ₑ D} (η : F ⟶ G) (H : D ⥤ₑ E) (c : C) :

(((whiskeringLeft C D E).map η).app H).app c = H.obj.map (η.app c)

source

def CategoryTheory.ExactFunctor.whiskeringRight (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] :

Functor (D ⥤ₑ E) (Functor (C ⥤ₑ D) (C ⥤ₑ E))

Whiskering an exact functor by an exact functor yields an exact functor.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_obj_map (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₑ E) {X✝ Y✝ : C ⥤ₑ D} (f : X✝ ⟶ Y✝) :

((whiskeringRight C D E).obj F).map f = whiskerRight f F.obj

source

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_map_app_app (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] {F G : D ⥤ₑ E} (η : F ⟶ G) (H : C ⥤ₑ D) (c : C) :

(((whiskeringRight C D E).map η).app H).app c = η.app (H.obj.obj c)

source

@[simp]

theorem CategoryTheory.ExactFunctor.whiskeringRight_obj_obj (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (E : Type u₃) [Category.{v₃, u₃} E] (F : D ⥤ₑ E) (X : C ⥤ₑ D) :

((whiskeringRight C D E).obj F).obj X = { obj := X.obj.comp F.obj, property := ⋯ }

Documentation

Mathlib.CategoryTheory.Limits.ExactFunctor

Bundled exact functors #