Ext #
We define Ext R C n : Cᵒᵖ ⥤ C ⥤ Module R for any R-linear abelian category C
by (left) deriving in the first argument of the bifunctor (X, Y) ↦ Module.of R (unop X ⟶ Y).
Implementation #
It's not actually necessary here to assume C is abelian,
but the hypotheses, involving both C and Cᵒᵖ, are quite lengthy,
and in practice the abelian case is hopefully enough.
PROJECT: State the alternative definition in terms of right deriving in the second argument, and show these agree.
@[simp]
theorem
Ext_obj
(R : Type u_1)
[ring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.abelian C]
[category_theory.linear R C]
[category_theory.enough_projectives C]
(n : ℕ)
(k : Cᵒᵖ) :
(Ext R C n).obj k = {obj := λ (j : C), opposite.unop ((((category_theory.linear_yoneda R C).obj j).right_op.left_derived n).obj (opposite.unop k)), map := λ (j j' : C) (f : j ⟶ j'), ((homotopy_category.homology_functor (Module R)ᵒᵖ (complex_shape.down ℕ) n).map ((homotopy_category.quotient (Module R)ᵒᵖ (complex_shape.down ℕ)).map ((category_theory.nat_trans.map_homological_complex (category_theory.nat_trans.right_op ((category_theory.linear_yoneda R C).map f)) (complex_shape.down ℕ)).app ((category_theory.projective_resolutions C).obj (opposite.unop k)).as))).unop, map_id' := _, map_comp' := _}
@[simp]
theorem
Ext_map
(R : Type u_1)
[ring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.abelian C]
[category_theory.linear R C]
[category_theory.enough_projectives C]
(n : ℕ)
(c c' : Cᵒᵖ)
(f : c ⟶ c') :
(Ext R C n).map f = {app := λ (j : C), ((((category_theory.linear_yoneda R C).obj j).right_op.left_derived n).map f.unop).unop, naturality' := _}
noncomputable
def
Ext
(R : Type u_1)
[ring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.abelian C]
[category_theory.linear R C]
[category_theory.enough_projectives C]
(n : ℕ) :
Ext R C n is defined by deriving in the first argument of (X, Y) ↦ Module.of R (unop X ⟶ Y)
(which is the second argument of linear_yoneda).
Equations
- Ext R C n = {obj := λ (Y : C), (((category_theory.linear_yoneda R C).obj Y).right_op.left_derived n).left_op, map := λ (Y Y' : C) (f : Y ⟶ Y'), category_theory.nat_trans.left_op (category_theory.nat_trans.left_derived (category_theory.nat_trans.right_op ((category_theory.linear_yoneda R C).map f)) n), map_id' := _, map_comp' := _}.flip
noncomputable
def
Ext_succ_of_projective
(R : Type u_1)
[ring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.abelian C]
[category_theory.linear R C]
[category_theory.enough_projectives C]
(X Y : C)
[category_theory.projective X]
(n : ℕ) :
If X : C is projective and n : ℕ, then Ext^(n + 1) X Y ≅ 0 for any Y.
Equations
- Ext_succ_of_projective R C X Y n = let E : opposite.unop ((((category_theory.linear_yoneda R C).obj Y).right_op.left_derived (n + 1)).obj X) ≅ opposite.unop 0 := (((category_theory.linear_yoneda R C).obj Y).right_op.left_derived_obj_projective_succ n X).unop.symm in E ≪≫ {hom := 0, inv := 0, hom_inv_id' := _, inv_hom_id' := _}