Rank-one maps on triangulated Grothendieck groups

An objectwise formula

[F X] = χ([X]) • e

is useful before a functor is known to be triangulated. K₀.IsRankOne packages that formula without asserting exactness. Once the usual hypotheses for K₀.map are available, the formula determines the induced homomorphism.

Here "rank one" means only that the displayed homomorphism factors through ℤ; neither χ nor e is required to be nonzero.

def CategoryTheory.Triangulated.K₀.rankOne {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (χ : K₀ C →+ ℤ) (e : K₀ D) : K₀ C →+ K₀ D

The homomorphism x ↦ χ(x) • e, factored through ℤ.

Equations

• CategoryTheory.Triangulated.K₀.rankOne χ e = ((smulAddHom ℤ (CategoryTheory.Triangulated.K₀ D)).flip e).comp χ

@[simp]

theorem CategoryTheory.Triangulated.K₀.rankOne_apply {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (χ : K₀ C →+ ℤ) (e : K₀ D) (x : K₀ C) : (rankOne χ e) x = χ x • e

def CategoryTheory.Triangulated.K₀.IsRankOne {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) (χ : K₀ C →+ ℤ) (e : K₀ D) : Prop

The object classes of F satisfy the rank-one formula determined by χ and e. This property does not assert that F is triangulated.

Equations

• CategoryTheory.Triangulated.K₀.IsRankOne F χ e = ∀ (X : C), CategoryTheory.Triangulated.K₀.of D (F.obj X) = χ (CategoryTheory.Triangulated.K₀.of C X) • e

theorem CategoryTheory.Triangulated.K₀.IsRankOne.ofIso {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {F G : Functor C D} {χ : K₀ C →+ ℤ} {e : K₀ D} (hF : IsRankOne F χ e) (i : F ≅ G) : IsRankOne G χ e

The rank-one object formula is invariant under natural isomorphism.

theorem CategoryTheory.Triangulated.K₀.IsRankOne.map_eq_rankOne {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {F : Functor C D} {χ : K₀ C →+ ℤ} {e : K₀ D} (hF : IsRankOne F χ e) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] : map F = rankOne χ e

Under the hypotheses that make K₀.map F available, the objectwise rank-one formula determines that homomorphism.