mathlib3 documentation

category_theory.limits.exact_functor

Bundled exact functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
@[protected, instance]
def category_theory.LeftExactFunctor.category (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.category (C ⥤ₗ D)
source
@[nolint]
def category_theory.LeftExactFunctor (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
Type (max v₁ v₂ u₁ u₂)

Bundled left-exact functors.

Equations
Instances for category_theory.LeftExactFunctor
source
@[protected, instance]
def category_theory.LeftExactFunctor.forget.faithful (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.faithful (category_theory.LeftExactFunctor.forget C D)
source
def category_theory.LeftExactFunctor.forget (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(C ⥤ₗ D) ⥤ C ⥤ D

A left exact functor is in particular a functor.

Equations
Instances for category_theory.LeftExactFunctor.forget
source
@[protected, instance]
def category_theory.LeftExactFunctor.forget.full (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.full (category_theory.LeftExactFunctor.forget C D)
source
@[protected, instance]
def category_theory.RightExactFunctor.category (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.category (C ⥤ᵣ D)
source
@[nolint]
def category_theory.RightExactFunctor (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
Type (max v₁ v₂ u₁ u₂)

Bundled right-exact functors.

Equations
Instances for category_theory.RightExactFunctor
source
@[protected, instance]
def category_theory.RightExactFunctor.forget.faithful (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.faithful (category_theory.RightExactFunctor.forget C D)
source
def category_theory.RightExactFunctor.forget (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(C ⥤ᵣ D) ⥤ C ⥤ D

A right exact functor is in particular a functor.

Equations
Instances for category_theory.RightExactFunctor.forget
source
@[protected, instance]
def category_theory.RightExactFunctor.forget.full (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.full (category_theory.RightExactFunctor.forget C D)
source
@[protected, instance]
def category_theory.ExactFunctor.category (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.category (C ⥤ₑ D)
source
@[nolint]
def category_theory.ExactFunctor (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
Type (max v₁ v₂ u₁ u₂)

Bundled exact functors.

Equations
Instances for category_theory.ExactFunctor
source
def category_theory.ExactFunctor.forget (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(C ⥤ₑ D) ⥤ C ⥤ D

An exact functor is in particular a functor.

Equations
Instances for category_theory.ExactFunctor.forget
source
@[protected, instance]
def category_theory.ExactFunctor.forget.faithful (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.faithful (category_theory.ExactFunctor.forget C D)
source
@[protected, instance]
def category_theory.ExactFunctor.forget.full (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.full (category_theory.ExactFunctor.forget C D)
source
@[protected, instance]
def category_theory.LeftExactFunctor.of_exact.full (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.full (category_theory.LeftExactFunctor.of_exact C D)
source
@[protected, instance]
def category_theory.LeftExactFunctor.of_exact.faithful (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.faithful (category_theory.LeftExactFunctor.of_exact C D)
source
def category_theory.LeftExactFunctor.of_exact (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(C ⥤ₑ D) ⥤ C ⥤ₗ D

Turn an exact functor into a left exact functor.

Equations
Instances for category_theory.LeftExactFunctor.of_exact
source
@[protected, instance]
def category_theory.RightExactFunctor.of_exact.faithful (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.faithful (category_theory.RightExactFunctor.of_exact C D)
source
def category_theory.RightExactFunctor.of_exact (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
(C ⥤ₑ D) ⥤ C ⥤ᵣ D

Turn an exact functor into a left exact functor.

Equations
Instances for category_theory.RightExactFunctor.of_exact
source
@[protected, instance]
def category_theory.RightExactFunctor.of_exact.full (C : Type u₁) [category_theory.category C] (D : Type u₂) [category_theory.category D] :
category_theory.full (category_theory.RightExactFunctor.of_exact C D)
source
@[simp]
theorem category_theory.LeftExactFunctor.of_exact_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ₑ D) :
(category_theory.LeftExactFunctor.of_exact C D).obj F = {obj := F.obj, property := _}
source
@[simp]
theorem category_theory.RightExactFunctor.of_exact_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ₑ D) :
(category_theory.RightExactFunctor.of_exact C D).obj F = {obj := F.obj, property := _}
source
@[simp]
theorem category_theory.LeftExactFunctor.of_exact_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ₑ D} (α : F ⟶ G) :
(category_theory.LeftExactFunctor.of_exact C D).map α = α
source
@[simp]
theorem category_theory.RightExactFunctor.of_exact_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ₑ D} (α : F ⟶ G) :
(category_theory.RightExactFunctor.of_exact C D).map α = α
source
@[simp]
theorem category_theory.LeftExactFunctor.forget_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ₗ D) :
(category_theory.LeftExactFunctor.forget C D).obj F = F.obj
source
@[simp]
theorem category_theory.RightExactFunctor.forget_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ᵣ D) :
(category_theory.RightExactFunctor.forget C D).obj F = F.obj
source
@[simp]
theorem category_theory.ExactFunctor.forget_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ₑ D) :
(category_theory.ExactFunctor.forget C D).obj F = F.obj
source
@[simp]
theorem category_theory.LeftExactFunctor.forget_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ₗ D} (α : F ⟶ G) :
(category_theory.LeftExactFunctor.forget C D).map α = α
source
@[simp]
theorem category_theory.RightExactFunctor.forget_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ᵣ D} (α : F ⟶ G) :
(category_theory.RightExactFunctor.forget C D).map α = α
source
@[simp]
theorem category_theory.ExactFunctor.forget_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F G : C ⥤ₑ D} (α : F ⟶ G) :
(category_theory.ExactFunctor.forget C D).map α = α
source
def category_theory.LeftExactFunctor.of {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] :
C ⥤ₗ D

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

Equations
source
def category_theory.RightExactFunctor.of {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_colimits F] :
C ⥤ᵣ D

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

Equations
source
def category_theory.ExactFunctor.of {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] [category_theory.limits.preserves_finite_colimits F] :
C ⥤ₑ D

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

Equations
source
@[simp]
theorem category_theory.LeftExactFunctor.of_fst {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] :
(category_theory.LeftExactFunctor.of F).obj = F
source
@[simp]
theorem category_theory.RightExactFunctor.of_fst {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_colimits F] :
(category_theory.RightExactFunctor.of F).obj = F
source
@[simp]
theorem category_theory.ExactFunctor.of_fst {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] [category_theory.limits.preserves_finite_colimits F] :
(category_theory.ExactFunctor.of F).obj = F
source
theorem category_theory.LeftExactFunctor.forget_obj_of {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] :
(category_theory.LeftExactFunctor.forget C D).obj (category_theory.LeftExactFunctor.of F) = F
source
theorem category_theory.RightExactFunctor.forget_obj_of {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_colimits F] :
(category_theory.RightExactFunctor.forget C D).obj (category_theory.RightExactFunctor.of F) = F
source
theorem category_theory.ExactFunctor.forget_obj_of {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_finite_limits F] [category_theory.limits.preserves_finite_colimits F] :
(category_theory.ExactFunctor.forget C D).obj (category_theory.ExactFunctor.of F) = F
source
@[protected, instance]
noncomputable def category_theory.LeftExactFunctor.obj.limits.preserves_finite_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ₗ D) :
category_theory.limits.preserves_finite_limits F.obj
Equations
source
@[protected, instance]
noncomputable def category_theory.RightExactFunctor.obj.limits.preserves_finite_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ᵣ D) :
category_theory.limits.preserves_finite_colimits F.obj
Equations
source
@[protected, instance]
noncomputable def category_theory.ExactFunctor.obj.limits.preserves_finite_limits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ₑ D) :
category_theory.limits.preserves_finite_limits F.obj
Equations
source
@[protected, instance]
noncomputable def category_theory.ExactFunctor.obj.limits.preserves_finite_colimits {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ₑ D) :
category_theory.limits.preserves_finite_colimits F.obj
Equations