Length-two projective resolutions of module cokernels

For maps f : P₂ →ₗ[A] P₁ and g : P₁ →ₗ[A] P₀ whose composite is zero, ModuleCatLengthTwo.complex is the chain complex supported in degrees zero, one and two. If the modules are projective, f is injective and range f = ker g, ModuleCatLengthTwo.projectiveResolution resolves P₀ ⧸ range g.

This packages the categorical assembly used by the signed and signless preprojective Koszul resolutions.

References

• TauCeti.RepresentationTheory.Quiver.Preprojective.Resolution, for the categorical assembly of the signed preprojective Koszul resolution.

@[reducible, inline]

noncomputable abbrev TauCeti.ModuleCatLengthTwo.term {A : Type u} [Ring A] (P₀ P₁ P₂ : Type v) [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] : ℕ → ModuleCat A

The three given modules in degrees zero, one and two, followed by zero modules.

noncomputable def TauCeti.ModuleCatLengthTwo.differential {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (n : ℕ) : term P₀ P₁ P₂ (n + 1) ⟶ term P₀ P₁ P₂ n

The given maps as consecutive differentials, followed by zero maps.

@[simp]

theorem TauCeti.ModuleCatLengthTwo.differential_zero {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) : differential f g 0 = ModuleCat.ofHom g

@[simp]

theorem TauCeti.ModuleCatLengthTwo.differential_one {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) : differential f g 1 = ModuleCat.ofHom f

@[simp]

theorem TauCeti.ModuleCatLengthTwo.differential_add_two {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (n : ℕ) : differential f g (n + 2) = 0

noncomputable def TauCeti.ModuleCatLengthTwo.complex {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hcomp : g ∘ₗ f = 0) : ChainComplex (ModuleCat A) ℕ

The chain complex with the specified three modules and two differentials.

@[simp]

theorem TauCeti.ModuleCatLengthTwo.complex_X {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hcomp : g ∘ₗ f = 0) (n : ℕ) : (complex f g hcomp).X n = term P₀ P₁ P₂ n

The terms of the bundled complex are the specified modules.

noncomputable def TauCeti.ModuleCatLengthTwo.complexXIso {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hcomp : g ∘ₗ f = 0) (n : ℕ) : (complex f g hcomp).X n ≅ term P₀ P₁ P₂ n

The bundled terms identified with the three specified modules.

@[simp]

theorem TauCeti.ModuleCatLengthTwo.complex_d {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hcomp : g ∘ₗ f = 0) (n : ℕ) : (complex f g hcomp).d (n + 1) n = CategoryTheory.CategoryStruct.comp (complexXIso f g hcomp (n + 1)).hom (CategoryTheory.CategoryStruct.comp (differential f g n) (complexXIso f g hcomp n).inv)

The bundled differential is the specified linear map.

noncomputable def TauCeti.ModuleCatLengthTwo.augmentation {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hcomp : g ∘ₗ f = 0) : complex f g hcomp ⟶ (ChainComplex.single₀ (ModuleCat A)).obj ↧(P₀ ⧸ g.range)

The quotient map augments the three-term complex to the cokernel of its last map.

@[simp]

theorem TauCeti.ModuleCatLengthTwo.augmentation_f_zero {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hcomp : g ∘ₗ f = 0) : CategoryTheory.CategoryStruct.comp (complexXIso f g hcomp 0).inv ((augmentation f g hcomp).f 0) = ModuleCat.ofHom g.range.mkQ

The augmentation in degree zero is the cokernel quotient map.

noncomputable def TauCeti.ModuleCatLengthTwo.projectiveResolution {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hexact : f.range = g.ker) (hinj : Function.Injective ⇑f) [Module.Projective A P₀] [Module.Projective A P₁] [Module.Projective A P₂] : CategoryTheory.ProjectiveResolution ↧(P₀ ⧸ g.range)

An exact three-term complex of projective modules with injective first map resolves its cokernel, with the given maps as differentials and the quotient map as augmentation.

@[simp]

theorem TauCeti.ModuleCatLengthTwo.projectiveResolution_complex {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hcomp : g ∘ₗ f = 0) (hexact : f.range = g.ker) (hinj : Function.Injective ⇑f) [Module.Projective A P₀] [Module.Projective A P₁] [Module.Projective A P₂] : (projectiveResolution f g hexact hinj).complex = complex f g hcomp

The resolution uses the specified three-term complex.

noncomputable def TauCeti.ModuleCatLengthTwo.projectiveResolutionXIso {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hexact : f.range = g.ker) (hinj : Function.Injective ⇑f) [Module.Projective A P₀] [Module.Projective A P₁] [Module.Projective A P₂] (n : ℕ) : (projectiveResolution f g hexact hinj).complex.X n ≅ term P₀ P₁ P₂ n

The projective terms of the resolution identified with the given modules.

@[simp]

theorem TauCeti.ModuleCatLengthTwo.projectiveResolution_d {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hexact : f.range = g.ker) (hinj : Function.Injective ⇑f) [Module.Projective A P₀] [Module.Projective A P₁] [Module.Projective A P₂] (n : ℕ) : (projectiveResolution f g hexact hinj).complex.d (n + 1) n = CategoryTheory.CategoryStruct.comp (projectiveResolutionXIso f g hexact hinj (n + 1)).hom (CategoryTheory.CategoryStruct.comp (differential f g n) (projectiveResolutionXIso f g hexact hinj n).inv)

The resolution differentials are the given linear maps, using the term identifications.

@[simp]

theorem TauCeti.ModuleCatLengthTwo.projectiveResolution_π_f_zero {A : Type u} [Ring A] {P₀ P₁ P₂ : Type v} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup P₂] [Module A P₂] (f : P₂ →ₗ[A] P₁) (g : P₁ →ₗ[A] P₀) (hexact : f.range = g.ker) (hinj : Function.Injective ⇑f) [Module.Projective A P₀] [Module.Projective A P₁] [Module.Projective A P₂] : CategoryTheory.CategoryStruct.comp (projectiveResolutionXIso f g hexact hinj 0).inv ((projectiveResolution f g hexact hinj).π.f 0) = ModuleCat.ofHom g.range.mkQ

The zeroth resolution map is the cokernel quotient map.