Map Between Ext Induced by Exact Functor #
In this file, we develope the map Ext^k (M, N) → Ext^k (F(M), F(N)),
where F is an exact functor between abelian categories.
instance
CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[h : HasExt D]
(X Y : C)
:
Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso D (ComplexShape.up ℤ)) ℤ
((F.comp (CochainComplex.singleFunctor D 0)).obj X) ((F.comp (CochainComplex.singleFunctor D 0)).obj Y)
noncomputable def
CategoryTheory.Abelian.Ext.mapExactFunctor
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
{X Y : C}
{n : ℕ}
(f : Ext X Y n)
:
The map between Ext induced by F.mapShiftedHomAddHom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Abelian.Ext.mapExactFunctor_hom
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasDerivedCategory C]
[HasDerivedCategory D]
[HasExt C]
[HasExt D]
{X Y : C}
{n : ℕ}
(e : Ext X Y n)
:
(mapExactFunctor F e).hom = CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X)
(CategoryStruct.comp (e.hom.map F.mapDerivedCategory)
((shiftFunctor (DerivedCategory D) ↑n).map ((F.mapDerivedCategorySingleFunctor 0).hom.app Y)))
@[simp]
theorem
CategoryTheory.Abelian.Ext.mapExactFunctor_zero
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
:
@[simp]
theorem
CategoryTheory.Abelian.Ext.mapExactFunctor_add
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
(f g : Ext X Y n)
:
noncomputable def
CategoryTheory.Functor.mapExtAddHom
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
:
The additive homomorphism between Ext induced by F.mapShiftedHomAddHom.
Equations
- F.mapExtAddHom X Y n = { toFun := fun (e : CategoryTheory.Abelian.Ext X Y n) => CategoryTheory.Abelian.Ext.mapExactFunctor F e, map_zero' := ⋯, map_add' := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapExtAddHom_coe
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
:
theorem
CategoryTheory.Functor.mapExtAddHom_apply
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
(e : Abelian.Ext X Y n)
:
@[simp]
theorem
CategoryTheory.Functor.mapExactFunctor_smul
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
(R : Type u_1)
[Ring R]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
[Linear R F]
(r : R)
(f : Abelian.Ext X Y n)
:
noncomputable def
CategoryTheory.Functor.mapExtLinearMap
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
(R : Type u_1)
[Ring R]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
[Linear R F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
:
Upgrade of F.mapExtAddHom assuming F is linear.
Equations
- F.mapExtLinearMap R X Y n = { toFun := (↑(F.mapExtAddHom X Y n)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapExtLinearMap_toAddMonoidHom
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
(R : Type u_1)
[Ring R]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
[Linear R F]
:
theorem
CategoryTheory.Functor.mapExtLinearMap_coe
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
(R : Type u_1)
[Ring R]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
[Linear R F]
:
theorem
CategoryTheory.Functor.mapExtLinearMap_apply
{C : Type u}
[Category.{v, u} C]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
(F : Functor C D)
[F.Additive]
[Limits.PreservesFiniteLimits F]
[Limits.PreservesFiniteColimits F]
[HasExt C]
[HasExt D]
(X Y : C)
(n : ℕ)
(R : Type u_1)
[Ring R]
[CategoryTheory.Linear R C]
[CategoryTheory.Linear R D]
[Linear R F]
(e : Abelian.Ext X Y n)
: