Adjunctions between exact functors and Ext-groups

Assume that adj : F ⊣ G is an adjunction between two exact functors F : C ⥤ D and G : D ⥤ C between abelian categories. In this file, we promote the bijection adj.homEquiv X Y : (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y) into additive equivalences adj.extEquiv : Ext (F.obj X) Y n ≃+ Ext X (G.obj Y) n.

noncomputable def CategoryTheory.Adjunction.extEquiv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y : D} {n : ℕ} : Abelian.Ext (F.obj X) Y n ≃+ Abelian.Ext X (G.obj Y) n

The bijection of Ext-groups that is induced by an adjunction between exact functors.

Equations

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

theorem CategoryTheory.Adjunction.extEquiv_apply {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y : D} {n : ℕ} (e : Abelian.Ext (F.obj X) Y n) : adj.extEquiv e = (Abelian.Ext.mk₀ (adj.unit.app X)).comp (Abelian.Ext.mapExactFunctor G e) ⋯

theorem CategoryTheory.Adjunction.extEquiv_symm_apply {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y : D} {n : ℕ} (e : Abelian.Ext X (G.obj Y) n) : adj.extEquiv.symm e = (Abelian.Ext.mapExactFunctor F e).comp (Abelian.Ext.mk₀ (adj.counit.app Y)) ⋯

@[simp]

theorem CategoryTheory.Adjunction.extEquiv_mk₀ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y : D} (f : F.obj X ⟶ Y) : adj.extEquiv (Abelian.Ext.mk₀ f) = Abelian.Ext.mk₀ ((adj.homEquiv X Y) f)

theorem CategoryTheory.Adjunction.extEquiv_symm_mk₀ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y : D} (f : X ⟶ G.obj Y) : adj.extEquiv.symm (Abelian.Ext.mk₀ f) = Abelian.Ext.mk₀ ((adj.homEquiv X Y).symm f)

@[simp]

theorem CategoryTheory.Adjunction.extEquiv_symm_mk₀_unit_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) (X : C) : adj.extEquiv.symm (Abelian.Ext.mk₀ (adj.unit.app X)) = Abelian.Ext.mk₀ (CategoryStruct.id (F.obj X))

@[simp]

theorem CategoryTheory.Adjunction.extEquiv_mk₀_counit_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) (Y : D) : adj.extEquiv (Abelian.Ext.mk₀ (adj.counit.app Y)) = Abelian.Ext.mk₀ (CategoryStruct.id (G.obj Y))

theorem CategoryTheory.Adjunction.extEquiv_naturality_left {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X₁ X₂ : C} {Y : D} {a b : ℕ} (e : Abelian.Ext X₁ X₂ a) (e' : Abelian.Ext (F.obj X₂) Y b) {c : ℕ} (h : a + b = c) : adj.extEquiv ((Abelian.Ext.mapExactFunctor F e).comp e' h) = e.comp (adj.extEquiv e') h

theorem CategoryTheory.Adjunction.extEquiv_naturality_left₀ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X₁ X₂ : C} {Y : D} (f : X₁ ⟶ X₂) {n : ℕ} (e : Abelian.Ext (F.obj X₂) Y n) : adj.extEquiv ((Abelian.Ext.mk₀ (F.map f)).comp e ⋯) = (Abelian.Ext.mk₀ f).comp (adj.extEquiv e) ⋯

theorem CategoryTheory.Adjunction.extEquiv_naturality_right {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {a b : ℕ} (e : Abelian.Ext (F.obj X) Y₁ a) (e' : Abelian.Ext Y₁ Y₂ b) {c : ℕ} (h : a + b = c) : adj.extEquiv (e.comp e' h) = (adj.extEquiv e).comp (Abelian.Ext.mapExactFunctor G e') h

theorem CategoryTheory.Adjunction.extEquiv_naturality_right₀ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {n : ℕ} (e : Abelian.Ext (F.obj X) Y₁ n) (f : Y₁ ⟶ Y₂) : adj.extEquiv (e.comp (Abelian.Ext.mk₀ f) ⋯) = (adj.extEquiv e).comp (Abelian.Ext.mk₀ (G.map f)) ⋯

theorem CategoryTheory.Adjunction.extEquiv_symm_naturality_left {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X₁ X₂ : C} {Y : D} {a b : ℕ} (e : Abelian.Ext X₁ X₂ a) (e' : Abelian.Ext X₂ (G.obj Y) b) {c : ℕ} (h : a + b = c) : adj.extEquiv.symm (e.comp e' h) = (Abelian.Ext.mapExactFunctor F e).comp (adj.extEquiv.symm e') h

theorem CategoryTheory.Adjunction.extEquiv_symm_naturality_left₀ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X₁ X₂ : C} {Y : D} {n : ℕ} (f : X₁ ⟶ X₂) (e : Abelian.Ext X₂ (G.obj Y) n) : adj.extEquiv.symm ((Abelian.Ext.mk₀ f).comp e ⋯) = (Abelian.Ext.mk₀ (F.map f)).comp (adj.extEquiv.symm e) ⋯

theorem CategoryTheory.Adjunction.extEquiv_symm_naturality_right {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {a b : ℕ} (e : Abelian.Ext X (G.obj Y₁) a) (e' : Abelian.Ext Y₁ Y₂ b) {c : ℕ} (h : a + b = c) : adj.extEquiv.symm (e.comp (Abelian.Ext.mapExactFunctor G e') h) = (adj.extEquiv.symm e).comp e' h

theorem CategoryTheory.Adjunction.extEquiv_symm_naturality_right₀ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) {X : C} {Y₁ Y₂ : D} {n : ℕ} (e : Abelian.Ext X (G.obj Y₁) n) (f : Y₁ ⟶ Y₂) : adj.extEquiv.symm (e.comp (Abelian.Ext.mk₀ (G.map f)) ⋯) = (adj.extEquiv.symm e).comp (Abelian.Ext.mk₀ f) ⋯

@[reducible, inline]

noncomputable abbrev CategoryTheory.Adjunction.extLinearEquiv {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] [HasExt C] [HasExt D] {F : Functor C D} {G : Functor D C} [F.Additive] [G.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) (R : Type u_3) [Ring R] [Linear R C] [Linear R D] [Functor.Linear R G] {X : C} {Y : D} {n : ℕ} : Abelian.Ext (F.obj X) Y n ≃ₗ[R] Abelian.Ext X (G.obj Y) n

The linear equivalence on Ext-modules that is induced by an adjunction between exact linear functors.

Equations

• adj.extLinearEquiv R = { toFun := adj.extEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := adj.extEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }