The category of graded objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For any type β, a β-graded object over some category C is just
a function β → C into the objects of C.
We put the "pointwise" category structure on these, as the non-dependent specialization of
category_theory.pi.
We describe the comap functors obtained by precomposing with functions β → γ.
As a consequence a fixed element (e.g. 1) in an additive group β provides a shift
functor on β-graded objects
When C has coproducts we construct the total functor graded_object β C ⥤ C,
show that it is faithful, and deduce that when C is concrete so is graded_object β C.
A type synonym for β → C, used for β-graded objects in a category C.
Equations
- category_theory.graded_object β C = (β → C)
Instances for category_theory.graded_object
- category_theory.inhabited_graded_object
- category_theory.graded_object.category_of_graded_objects
- category_theory.graded_object.has_shift
- category_theory.graded_object.has_zero_morphisms
- category_theory.graded_object.has_zero_object
- category_theory.graded_object.category_theory.concrete_category
- category_theory.graded_object.category_theory.has_forget₂
@[protected, instance]
Equations
- category_theory.inhabited_graded_object β C = {default := λ (b : β), inhabited.default}
@[nolint, reducible]
def
category_theory.graded_object_with_shift
{β : Type w}
[add_comm_group β]
(s : β)
(C : Type u) :
Type (max w u)
A type synonym for β → C, used for β-graded objects in a category C
with a shift functor given by translation by s.
@[protected, instance]
def
category_theory.graded_object.category_of_graded_objects
{C : Type u}
[category_theory.category C]
(β : Type w) :
Equations
- category_theory.graded_object.category_of_graded_objects β = category_theory.pi (λ (_x : β), C)
def
category_theory.graded_object.eval
{C : Type u}
[category_theory.category C]
{β : Type w}
(b : β) :
The projection of a graded object to its i-th component.
Equations
- category_theory.graded_object.eval b = {obj := λ (X : category_theory.graded_object β C), X b, map := λ (X Y : category_theory.graded_object β C) (f : X ⟶ Y), f b, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.graded_object.eval_obj
{C : Type u}
[category_theory.category C]
{β : Type w}
(b : β)
(X : category_theory.graded_object β C) :
(category_theory.graded_object.eval b).obj X = X b
@[simp]
theorem
category_theory.graded_object.eval_map
{C : Type u}
[category_theory.category C]
{β : Type w}
(b : β)
(X Y : category_theory.graded_object β C)
(f : X ⟶ Y) :
(category_theory.graded_object.eval b).map f = f b
@[simp]
theorem
category_theory.graded_object.comap_eq_hom_app
(C : Type u)
[category_theory.category C]
{β γ : Type w}
{f g : β → γ}
(h : f = g)
(X : γ → C)
(b : β) :
def
category_theory.graded_object.comap_eq
(C : Type u)
[category_theory.category C]
{β γ : Type w}
{f g : β → γ}
(h : f = g) :
category_theory.pi.comap (λ (_x : γ), C) f ≅ category_theory.pi.comap (λ (_x : γ), C) g
The natural isomorphism comparing between pulling back along two propositionally equal functions.
Equations
- category_theory.graded_object.comap_eq C h = {hom := {app := λ (X : γ → C) (b : β), category_theory.eq_to_hom _, naturality' := _}, inv := {app := λ (X : γ → C) (b : β), category_theory.eq_to_hom _, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.graded_object.comap_eq_inv_app
(C : Type u)
[category_theory.category C]
{β γ : Type w}
{f g : β → γ}
(h : f = g)
(X : γ → C)
(b : β) :
theorem
category_theory.graded_object.comap_eq_symm
(C : Type u)
[category_theory.category C]
{β γ : Type w}
{f g : β → γ}
(h : f = g) :
theorem
category_theory.graded_object.comap_eq_trans
(C : Type u)
[category_theory.category C]
{β γ : Type w}
{f g h : β → γ}
(k : f = g)
(l : g = h) :
@[simp]
theorem
category_theory.graded_object.eq_to_hom_apply
(C : Type u)
[category_theory.category C]
{β : Type w}
{X Y : β → C}
(h : X = Y)
(b : β) :
def
category_theory.graded_object.comap_equiv
(C : Type u)
[category_theory.category C]
{β γ : Type w}
(e : β ≃ γ) :
The equivalence between β-graded objects and γ-graded objects, given an equivalence between β and γ.
Equations
- category_theory.graded_object.comap_equiv C e = {functor := category_theory.pi.comap (λ (_x : β), C) ⇑(e.symm), inverse := category_theory.pi.comap (λ (_x : γ), C) ⇑e, unit_iso := category_theory.graded_object.comap_eq C _ ≪≫ (category_theory.pi.comap_comp (λ (_x : β), C) ⇑e ⇑(e.symm)).symm, counit_iso := category_theory.pi.comap_comp (λ (_x : γ), C) ⇑(e.symm) ⇑e ≪≫ category_theory.graded_object.comap_eq C _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.graded_object.comap_equiv_functor
(C : Type u)
[category_theory.category C]
{β γ : Type w}
(e : β ≃ γ) :
(category_theory.graded_object.comap_equiv C e).functor = category_theory.pi.comap (λ (_x : β), C) ⇑(e.symm)
@[simp]
theorem
category_theory.graded_object.comap_equiv_counit_iso
(C : Type u)
[category_theory.category C]
{β γ : Type w}
(e : β ≃ γ) :
(category_theory.graded_object.comap_equiv C e).counit_iso = category_theory.pi.comap_comp (λ (_x : γ), C) ⇑(e.symm) ⇑e ≪≫ category_theory.graded_object.comap_eq C _
@[simp]
theorem
category_theory.graded_object.comap_equiv_inverse
(C : Type u)
[category_theory.category C]
{β γ : Type w}
(e : β ≃ γ) :
(category_theory.graded_object.comap_equiv C e).inverse = category_theory.pi.comap (λ (_x : γ), C) ⇑e
@[simp]
theorem
category_theory.graded_object.comap_equiv_unit_iso
(C : Type u)
[category_theory.category C]
{β γ : Type w}
(e : β ≃ γ) :
(category_theory.graded_object.comap_equiv C e).unit_iso = category_theory.graded_object.comap_eq C _ ≪≫ (category_theory.pi.comap_comp (λ (_x : β), C) ⇑e ⇑(e.symm)).symm
@[protected, instance]
def
category_theory.graded_object.has_shift
{C : Type u}
[category_theory.category C]
{β : Type u_1}
[add_comm_group β]
(s : β) :
Equations
- category_theory.graded_object.has_shift s = category_theory.has_shift_mk (category_theory.graded_object_with_shift s C) ℤ {F := λ (n : ℤ), category_theory.pi.comap (λ (_x : β), C) (λ (b : β), b + n • s), zero := category_theory.graded_object.comap_eq C _ ≪≫ category_theory.pi.comap_id β (λ (_x : β), C), add := λ (m n : ℤ), category_theory.graded_object.comap_eq C _ ≪≫ (category_theory.pi.comap_comp (λ (_x : β), C) (λ (b : β), b + n • s) (λ (b : β), b + m • s)).symm, assoc_hom_app := _, zero_add_hom_app := _, add_zero_hom_app := _}
@[simp]
theorem
category_theory.graded_object.shift_functor_obj_apply
{C : Type u}
[category_theory.category C]
{β : Type u_1}
[add_comm_group β]
(s : β)
(X : β → C)
(t : β)
(n : ℤ) :
(category_theory.shift_functor (category_theory.graded_object_with_shift s C) n).obj X t = X (t + n • s)
@[simp]
theorem
category_theory.graded_object.shift_functor_map_apply
{C : Type u}
[category_theory.category C]
{β : Type u_1}
[add_comm_group β]
(s : β)
{X Y : category_theory.graded_object_with_shift s C}
(f : X ⟶ Y)
(t : β)
(n : ℤ) :
(category_theory.shift_functor (category_theory.graded_object_with_shift s C) n).map f t = f (t + n • s)
@[protected, instance]
def
category_theory.graded_object.has_zero_morphisms
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(β : Type w) :
Equations
- category_theory.graded_object.has_zero_morphisms β = {has_zero := λ (X Y : category_theory.graded_object β C), {zero := λ (b : β), 0}, comp_zero' := _, zero_comp' := _}
@[simp]
theorem
category_theory.graded_object.zero_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(β : Type w)
(X Y : category_theory.graded_object β C)
(b : β) :
0 b = 0
@[protected, instance]
noncomputable
def
category_theory.graded_object.total
(β : Type)
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_coproducts C] :
The total object of a graded object is the coproduct of the graded components.
Equations
- category_theory.graded_object.total β C = {obj := λ (X : category_theory.graded_object β C), ∐ λ (i : β), X i, map := λ (X Y : category_theory.graded_object β C) (f : X ⟶ Y), category_theory.limits.sigma.map (λ (i : β), f i), map_id' := _, map_comp' := _}
Instances for category_theory.graded_object.total
@[protected, instance]
def
category_theory.graded_object.total.category_theory.faithful
(β : Type)
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_zero_morphisms C] :
The total functor taking a graded object to the coproduct of its graded components is faithful.
To prove this, we need to know that the coprojections into the coproduct are monomorphisms,
which follows from the fact we have zero morphisms and decidable equality for the grading.
@[protected, instance]
noncomputable
def
category_theory.graded_object.category_theory.concrete_category
(β : Type)
(C : Type (u+1))
[category_theory.large_category C]
[category_theory.concrete_category C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_zero_morphisms C] :
@[protected, instance]
noncomputable
def
category_theory.graded_object.category_theory.has_forget₂
(β : Type)
(C : Type (u+1))
[category_theory.large_category C]
[category_theory.concrete_category C]
[category_theory.limits.has_coproducts C]
[category_theory.limits.has_zero_morphisms C] :