Map between Ext groups induced by an exact functor

In this file, we define the map Ext^k (M, N) → Ext^k (F(M), F(N)), where F is an exact functor between abelian categories.

Main Definition and results

• CategoryTheory.Abelian.Ext.mapExactFunctor : The map between Ext induced by CategoryTheory.LocalizerMorphism.smallShiftedHomMap.

• CategoryTheory.Functor.mapExtAddHom : Upgraded of CategoryTheory.Abelian.Ext.mapExactFunctor into an additive homomorphism.

• CategoryTheory.Functor.mapExtLinearMap : Upgrade of F.mapExtAddHom assuming F is linear.

• Ext.mapExactFunctor_mk₀ : Ext.mapExactFunctor commutes with Ext.mk₀

• Ext.mapExactFunctor_comp : Ext.mapExactFunctor preserves Ext.comp

• mapExactFunctor_extClass : Ext.mapExactFunctor commutes with ShortComplex.ShortExact.extClass

theorem CategoryTheory.DerivedCategory.map_triangleOfSESδ {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] {S : ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) : F.mapDerivedCategory.map (DerivedCategory.triangleOfSESδ hS) = CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app S.X₃) (CategoryStruct.comp (DerivedCategory.triangleOfSESδ ⋯) (CategoryStruct.comp ((shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁)) ((Functor.commShiftIso F.mapDerivedCategory 1).inv.app (DerivedCategory.Q.obj S.X₁))))

theorem CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ' {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : ShortComplex C} (hS : S.ShortExact) (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃) (CategoryStruct.comp (ShiftedHom.map hS.singleδ F.mapDerivedCategory) ((shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁))) = ⋯.singleδ

theorem CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ'_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : ShortComplex C} (hS : S.ShortExact) (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {Z : DerivedCategory D} (h : (shiftFunctor (DerivedCategory D) 1).obj ((DerivedCategory.singleFunctor D 0).obj (F.obj S.X₁)) ⟶ Z) : CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃) (CategoryStruct.comp (ShiftedHom.map hS.singleδ F.mapDerivedCategory) (CategoryStruct.comp ((shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁)) h)) = CategoryStruct.comp ⋯.singleδ h

theorem CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : ShortComplex C} (hS : S.ShortExact) (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : ShiftedHom.map hS.singleδ F.mapDerivedCategory = CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃) (CategoryStruct.comp ⋯.singleδ ((shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁)))

theorem CategoryTheory.ShortComplex.ShortExact.mapShiftedHom_singleδ_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] [HasDerivedCategory C] [HasDerivedCategory D] {S : ShortComplex C} (hS : S.ShortExact) (F : Functor C D) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {Z : DerivedCategory D} (h : (shiftFunctor (DerivedCategory D) 1).obj (F.mapDerivedCategory.obj ((DerivedCategory.singleFunctor C 0).obj S.X₁)) ⟶ Z) : CategoryStruct.comp (ShiftedHom.map hS.singleδ F.mapDerivedCategory) h = CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₃) (CategoryStruct.comp ⋯.singleδ (CategoryStruct.comp ((shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).inv.app S.X₁)) h))

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) : Ext (F.obj X) (F.obj Y) n

The map between Ext induced by LocalizerMorphism.smallShiftedHomMap.

Equations

• One or more equations did not get rendered due to their size.

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 : ℕ) : mapExactFunctor F 0 = 0

@[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) : mapExactFunctor F (f + g) = mapExactFunctor F f + mapExactFunctor F g

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 : ℕ) : Abelian.Ext X Y n →+ Abelian.Ext (F.obj X) (F.obj Y) n

Upgraded of CategoryTheory.Abelian.Ext.mapExactFunctor into an additive homomorphism.

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' := ⋯ }

@[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 : ℕ) : ⇑(F.mapExtAddHom X Y n) = Abelian.Ext.mapExactFunctor F

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) : (F.mapExtAddHom X Y n) e = Abelian.Ext.mapExactFunctor F e

@[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) : Abelian.Ext.mapExactFunctor F (r • f) = r • Abelian.Ext.mapExactFunctor F f

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] [HasExt C] [HasExt D] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [Linear R F] (X Y : C) (n : ℕ) : Abelian.Ext X Y n →ₗ[R] Abelian.Ext (F.obj X) (F.obj Y) 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' := ⋯ }

@[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] : ↑(F.mapExtLinearMap R X Y n) = F.mapExtAddHom X Y n

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] : ⇑(F.mapExtLinearMap R X Y n) = Abelian.Ext.mapExactFunctor 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) : (F.mapExtLinearMap R X Y n) e = Abelian.Ext.mapExactFunctor F e

theorem CategoryTheory.Abelian.Ext.mapExactFunctor_mk₀ {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} (f : X ⟶ Y) : mapExactFunctor F (mk₀ f) = mk₀ (F.map f)

theorem 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) : mapExactFunctor F = ⇑homEquiv₀.symm ∘ F.map ∘ ⇑homEquiv₀

theorem CategoryTheory.Abelian.Ext.mapExactFunctor_comp {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 Z : C} {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a + b = c) : mapExactFunctor F (α.comp β h) = (mapExactFunctor F α).comp (mapExactFunctor F β) h

theorem CategoryTheory.Abelian.Ext.mapExactFunctor_extClass {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] {S : ShortComplex C} (hS : S.ShortExact) : mapExactFunctor F hS.extClass = ⋯.extClass