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₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] :

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

Bundled left-exact functors.

Instances For

source

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

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

source

def CategoryTheory.«term_⥤ₗ_» :

Lean.TrailingParserDescr

C ⥤ₗ D denotes left exact functors C ⥤ D

Instances For

source

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

CategoryTheory.Functor (C ⥤ₗ D) (CategoryTheory.Functor C D)

A left exact functor is in particular a functor.

Instances For

source

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

CategoryTheory.Full (CategoryTheory.LeftExactFunctor.forget C D)

source

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

CategoryTheory.Faithful (CategoryTheory.LeftExactFunctor.forget C D)

source

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

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

Bundled right-exact functors.

Instances For

source

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

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

source

def CategoryTheory.«term_⥤ᵣ_» :

Lean.TrailingParserDescr

C ⥤ᵣ D denotes right exact functors C ⥤ D

Instances For

source

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

CategoryTheory.Functor (C ⥤ᵣ D) (CategoryTheory.Functor C D)

A right exact functor is in particular a functor.

Instances For

source

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

CategoryTheory.Full (CategoryTheory.RightExactFunctor.forget C D)

source

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

CategoryTheory.Faithful (CategoryTheory.RightExactFunctor.forget C D)

source

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

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

Bundled exact functors.

Instances For

source

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

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

source

def CategoryTheory.«term_⥤ₑ_» :

Lean.TrailingParserDescr

C ⥤ₑ D denotes exact functors C ⥤ D

Instances For

source

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

CategoryTheory.Functor (C ⥤ₑ D) (CategoryTheory.Functor C D)

An exact functor is in particular a functor.

Instances For

source

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

CategoryTheory.Full (CategoryTheory.ExactFunctor.forget C D)

source

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

CategoryTheory.Faithful (CategoryTheory.ExactFunctor.forget C D)

source

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

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

Turn an exact functor into a left exact functor.

Instances For

source

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

CategoryTheory.Full (CategoryTheory.LeftExactFunctor.ofExact C D)

source

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

CategoryTheory.Faithful (CategoryTheory.LeftExactFunctor.ofExact C D)

source

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

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

Turn an exact functor into a left exact functor.

Instances For

source

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

CategoryTheory.Full (CategoryTheory.RightExactFunctor.ofExact C D)

source

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

CategoryTheory.Faithful (CategoryTheory.RightExactFunctor.ofExact C D)

source

@[simp]

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

(CategoryTheory.LeftExactFunctor.ofExact C D).obj F = { obj := F.obj, property := (_ : Nonempty (CategoryTheory.Limits.PreservesFiniteLimits F.obj)) }

source

@[simp]

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

(CategoryTheory.RightExactFunctor.ofExact C D).obj F = { obj := F.obj, property := (_ : Nonempty (CategoryTheory.Limits.PreservesFiniteColimits F.obj)) }

source

@[simp]

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

(CategoryTheory.LeftExactFunctor.ofExact C D).map α = α

source

@[simp]

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

(CategoryTheory.RightExactFunctor.ofExact C D).map α = α

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(CategoryTheory.LeftExactFunctor.forget C D).map α = α

source

@[simp]

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

(CategoryTheory.RightExactFunctor.forget C D).map α = α

source

@[simp]

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

(CategoryTheory.ExactFunctor.forget C D).map α = α

source

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

C ⥤ₗ D

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

Instances For

source

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

C ⥤ᵣ D

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

Instances For

source

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

C ⥤ₑ D

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

Instances For

source

@[simp]

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

(CategoryTheory.LeftExactFunctor.of F).obj = F

source

@[simp]

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

(CategoryTheory.RightExactFunctor.of F).obj = F

source

@[simp]

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

(CategoryTheory.ExactFunctor.of F).obj = F

source

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

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

source

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

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

source

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

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

source

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

CategoryTheory.Limits.PreservesFiniteLimits F.obj

source

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

CategoryTheory.Limits.PreservesFiniteColimits F.obj

source

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

CategoryTheory.Limits.PreservesFiniteLimits F.obj

source

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

CategoryTheory.Limits.PreservesFiniteColimits F.obj