Exact K₀ of a Quillen exact category

The exact Grothendieck group TauCeti.ExactK0 E of an essentially small additive category C equipped with a Quillen exact structure E is the free abelian group on the isomorphism classes of objects modulo the relations [X₂] = [X₁] + [X₃], one for each E-conflation X₁ ↪ X₂ ↠ X₃. It is the universal recipient of an invariant which is constant on isomorphism classes and additive on conflations.

The construction is the presentation engine of TauCeti/CategoryTheory/GrothendieckGroup/Presentation.lean applied to the conflation relations, so the skeleton and shrink choices are made once and for all there, and the whole public API below is phrased in terms of objects and conflations of C.

Exact K₀ is monotone in the exact structure: an exact structure with more conflations imposes more relations, and TauCeti.ExactK0.ofLE is the resulting surjective comparison. The split exact structure is the smallest one (TauCeti.ExactStructure.conflation_of_splitting), so TauCeti.ExactK0.fromSplit compares TauCeti.SplitK0 C with the exact K₀ of an arbitrary exact structure on the same category. Both maps are characterized by their values on object classes, and both are natural in conflation-exact functors.

Main definitions

• TauCeti.conflationRelation S: the relation [X₂] - [X₁] - [X₃] attached to a short complex, and TauCeti.exactRelations E the family of those attached to the conflations of E.
• TauCeti.ExactK0 E: exact K₀, with class map TauCeti.ExactK0.of.
• TauCeti.ExactK0.AdditiveInvariant E G: an isomorphism-invariant, conflation-additive function on objects, and TauCeti.ExactK0.lift the homomorphism it induces.
• TauCeti.ExactK0.RightAdditiveInvariant C E' G: an object-level invariant additive on conflations in its second variable, and TauCeti.ExactK0.RightAdditiveInvariant.rightLift its one-sided descent.
• TauCeti.ExactK0.BiadditiveInvariant E E' G: a right-additive invariant which is also additive on conflations in its first variable, and TauCeti.ExactK0.BiadditiveInvariant.bilift its descent to both exact Grothendieck groups.
• TauCeti.ExactK0.map and TauCeti.ExactK0.mapEquiv: functoriality for conflation-exact functors and invariance under exact equivalences, with TauCeti.ExactK0.transportEquiv the instance of the latter for a transported exact structure.
• TauCeti.ExactK0.ofLE and TauCeti.ExactK0.fromSplit: the comparison induced by the identity functor towards an exact structure with more conflations, and its instance out of the split Grothendieck group; TauCeti.ExactK0.ofLEEquiv is the comparison isomorphism between exact structures with the same conflations.

Main results

• TauCeti.ExactK0.of_conflation: the defining relation, with TauCeti.ExactK0.of_biprod and TauCeti.ExactK0.of_eq_zero_of_isZero its biproduct and zero-object consequences.
• TauCeti.ExactK0.liftEquiv: the universal property. Conflation-additive invariants with values in G correspond bijectively to homomorphisms ExactK0 E →+ G.
• TauCeti.ExactK0.RightAdditiveInvariant.rightLift_of and TauCeti.ExactK0.RightAdditiveInvariant.rightLift_unique: evaluation and uniqueness of the one-sided descent.
• TauCeti.ExactK0.BiadditiveInvariant.bilift_of_of and TauCeti.ExactK0.BiadditiveInvariant.bilift_unique: evaluation and uniqueness of the two-variable descent.
• TauCeti.ExactK0.ofLE_unique and TauCeti.ExactK0.ofLE_surjective: the comparison map is the unique homomorphism preserving object classes, and it is surjective, so exact K₀ is a quotient of the exact K₀ of any smaller exact structure.
• TauCeti.ExactK0.fromSplitEquiv: if every conflation splits, the canonical comparison from split K₀ is an equivalence.
• TauCeti.ExactK0.map_comp_ofLE: naturality of the comparison in a conflation-exact functor.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 7, where K₀ of an exact category is presented by the conflation relations and its universal property for additive invariants is stated, and Section 6 for the presentation and the set-theoretic care taken in the engine consumed here.
• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, Section 13.1 for the split exact structure, the smallest one, whose comparison map is TauCeti.ExactK0.fromSplit.

noncomputable def TauCeti.conflationRelation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (S : CategoryTheory.ShortComplex C) : FreeAbelianGroup (ObjectCode C)

The relation [X₂] - [X₁] - [X₃] attached to a short complex. Exact K₀ imposes it for every conflation.

Equations

• TauCeti.conflationRelation S = TauCeti.freeOf S.X₂ - TauCeti.freeOf S.X₁ - TauCeti.freeOf S.X₃

@[simp]

theorem TauCeti.conflationRelation_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (S : CategoryTheory.ShortComplex C) : conflationRelation S = freeOf S.X₂ - freeOf S.X₁ - freeOf S.X₃

The defining equation of TauCeti.conflationRelation.

theorem TauCeti.map_conflationRelation_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddGroup G] (f : FreeAbelianGroup (ObjectCode C) →+ G) (S : CategoryTheory.ShortComplex C) : f (conflationRelation S) = 0 ↔ f (freeOf S.X₂) = f (freeOf S.X₁) + f (freeOf S.X₃)

An additive homomorphism annihilates the relation of a short complex exactly when it is additive on that complex. This evaluates a conflation relation once and for all, for both the quotient map presenting exact K₀ and the free extension of an invariant.

theorem TauCeti.freeMap_conflationRelation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C) : (freeMap F) (conflationRelation S) = conflationRelation (S.map F)

The free map of a functor carries the relation of a short complex to the relation of its image.

def TauCeti.exactRelations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : ExactStructure C) : Set (FreeAbelianGroup (ObjectCode C))

The family of conflation relations presenting the exact K₀ of an exact structure.

Equations

• TauCeti.exactRelations E = {r : FreeAbelianGroup (TauCeti.ObjectCode C) | ∃ (S : CategoryTheory.ShortComplex C), E.Conflation S ∧ r = TauCeti.conflationRelation S}

@[simp]

theorem TauCeti.mem_exactRelations_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {r : FreeAbelianGroup (ObjectCode C)} : r ∈ exactRelations E ↔ ∃ (S : CategoryTheory.ShortComplex C), E.Conflation S ∧ r = conflationRelation S

Membership in the family of conflation relations.

theorem TauCeti.conflationRelation_mem_exactRelations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) : conflationRelation S ∈ exactRelations E

theorem TauCeti.exactRelations_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S → E'.Conflation S) : exactRelations E ⊆ exactRelations E'

An exact structure with more conflations imposes more relations.

def TauCeti.ExactK0 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : ExactStructure C) : Type w

The Grothendieck group of a Quillen exact structure E on an essentially small additive category: the free abelian group on the isomorphism classes of objects, modulo [X₂] = [X₁] + [X₃] for every E-conflation X₁ ↪ X₂ ↠ X₃.

Equations

• TauCeti.ExactK0 E = TauCeti.PresentedK0 (TauCeti.exactRelations E)

@[instance_reducible]

instance TauCeti.instAddCommGroupExactK0 {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : ExactStructure C) : AddCommGroup (ExactK0 E)

Equations

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

noncomputable def TauCeti.ExactK0.of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} (X : C) : ExactK0 E

The class of an object in exact K₀.

Equations

• TauCeti.ExactK0.of X = TauCeti.PresentedK0.of X

theorem TauCeti.ExactK0.of_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {X Y : C} (e : X ≅ Y) : of X = of Y

theorem TauCeti.ExactK0.of_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) : of S.X₂ = of S.X₁ + of S.X₃

The defining relation of exact K₀: the class of the middle term of a conflation is the sum of the classes of its outer terms.

theorem TauCeti.ExactK0.of_eq_add_of_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {X Y Z : C} {i : X ⟶ Y} {p : Y ⟶ Z} (zero : CategoryTheory.CategoryStruct.comp i p = 0) (hS : E.Conflation { X₁ := X, X₂ := Y, X₃ := Z, f := i, g := p, zero := zero }) : of Y = of X + of Z

The defining relation of exact K₀, stated for a conflation presented by its two maps.

theorem TauCeti.ExactK0.of_conflation_fullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] (hP : E.IsExtensionClosed P) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) (h₁ : P S.X₁) (h₃ : P S.X₃) : of { obj := S.X₂, property := ⋯ } = of { obj := S.X₁, property := h₁ } + of { obj := S.X₃, property := h₃ }

An ambient conflation whose outer terms satisfy an extension-closed property gives the defining relation in the exact K₀ of the induced full subcategory.

theorem TauCeti.ExactK0.of_eq_sub_of_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) : of S.X₁ = of S.X₂ - of S.X₃

The class of the subobject of a conflation is the difference of the other two classes.

@[simp]

theorem TauCeti.ExactK0.of_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} (X Z : C) : of (X ⊞ Z) = of X + of Z

The class of a biproduct is the sum of the classes: every exact structure contains the biproduct conflations.

theorem TauCeti.ExactK0.of_biprod_fullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [CategoryTheory.EssentiallySmall.{w, v, u} P.FullSubcategory] (hP : E.IsExtensionClosed P) {X Y : C} (hX : P X) (hY : P Y) : of { obj := X ⊞ Y, property := ⋯ } = of { obj := X, property := hX } + of { obj := Y, property := hY }

The class of an explicitly presented ambient biproduct in the exact K₀ of an induced full subcategory is the sum of the classes of its summands. The middle object is the one supplied by closure under binary products; by proof irrelevance the statement applies to any presentation of it.

@[simp]

theorem TauCeti.ExactK0.of_eq_zero_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {X : C} (hX : CategoryTheory.Limits.IsZero X) : of X = 0

The class of an object which is zero vanishes.

@[simp]

theorem TauCeti.ExactK0.of_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} : of 0 = 0

The class of the zero object vanishes.

theorem TauCeti.ExactK0.closure_range_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} : AddSubgroup.closure (Set.range of) = ⊤

The image of the class map generates exact K₀.

theorem TauCeti.ExactK0.induction_on {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {motive : ExactK0 E → Prop} (x : ExactK0 E) (zero : motive 0) (of : ∀ (X : C), motive (of X)) (add : ∀ (a b : ExactK0 E), motive a → motive b → motive (a + b)) (neg : ∀ (a : ExactK0 E), motive a → motive (-a)) : motive x

Induction on the classes of objects of C: no skeleton representative is ever mentioned.

theorem TauCeti.ExactK0.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddMonoid G] {f g : ExactK0 E →+ G} (h : ∀ (X : C), f (of X) = g (of X)) : f = g

Two homomorphisms out of exact K₀ agreeing on the classes of objects are equal.

theorem TauCeti.ExactK0.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddMonoid G] {f g : ExactK0 E →+ G} : f = g ↔ ∀ (X : C), f (of X) = g (of X)

theorem TauCeti.ExactK0.surjective_of_forall_of_mem_range {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddGroup G] {f : G →+ ExactK0 E} (h : ∀ (X : C), of X ∈ f.range) : Function.Surjective ⇑f

A homomorphism into exact K₀ whose range contains the class of every object is surjective.

structure TauCeti.ExactK0.AdditiveInvariant {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (G : Type u_2) [AddCommGroup G] : Type (max u u_2)

An additive invariant for exact K₀: a function on objects of C additive on the conflations of E. It is then constant on isomorphism classes (TauCeti.ExactK0.AdditiveInvariant.map_iso). These are exactly the data that factor through TauCeti.ExactK0 E; see TauCeti.ExactK0.liftEquiv.

• obj : C → G

  The value of the invariant on an object.

• map_conflation ⦃S : CategoryTheory.ShortComplex C⦄ : E.Conflation S → self.obj S.X₂ = self.obj S.X₁ + self.obj S.X₃

  The value on the middle term of a conflation is the sum of the outer values.

theorem TauCeti.ExactK0.AdditiveInvariant.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts C} {E : ExactStructure C} {G : Type u_2} {inst✝⁴ : AddCommGroup G} {x y : AdditiveInvariant E G} (obj : x.obj = y.obj) : x = y

theorem TauCeti.ExactK0.AdditiveInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts C} {E : ExactStructure C} {G : Type u_2} {inst✝⁴ : AddCommGroup G} {x y : AdditiveInvariant E G} : x = y ↔ x.obj = y.obj

theorem TauCeti.ExactK0.AdditiveInvariant.map_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant E G) ⦃X Y : C⦄ (e : X ≅ Y) : a.obj X = a.obj Y

An additive invariant takes equal values on isomorphic objects. Additivity on conflations alone forces invariance under isomorphisms of objects, which is the invariance the presentation of exact K₀ requires.

theorem TauCeti.ExactK0.AdditiveInvariant.obj_eq_zero_of_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant E G) {X : C} (hX : CategoryTheory.Limits.IsZero X) : a.obj X = 0

An additive invariant vanishes on zero objects.

noncomputable def TauCeti.ExactK0.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant E G) : ExactK0 E →+ G

The homomorphism out of exact K₀ induced by a conflation-additive invariant.

Equations

• TauCeti.ExactK0.lift a = TauCeti.PresentedK0.lift (TauCeti.ExactK0.AdditiveInvariant.toPresented✝ a)

@[simp]

theorem TauCeti.ExactK0.lift_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant E G) (X : C) : (lift a) (of X) = a.obj X

theorem TauCeti.ExactK0.lift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant E G) (f : ExactK0 E →+ G) (hf : ∀ (X : C), f (of X) = a.obj X) : f = lift a

Any homomorphism agreeing with a conflation-additive invariant on object classes is its induced lift.

noncomputable def TauCeti.ExactK0.liftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] : AdditiveInvariant E G ≃ (ExactK0 E →+ G)

The universal property of exact K₀: conflation-additive invariants with values in G correspond bijectively to additive homomorphisms ExactK0 E →+ G.

Equations

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

@[simp]

theorem TauCeti.ExactK0.liftEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] (a : AdditiveInvariant E G) : liftEquiv a = lift a

@[simp]

theorem TauCeti.ExactK0.liftEquiv_symm_apply_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} {G : Type u_1} [AddCommGroup G] (f : ExactK0 E →+ G) (X : C) : (liftEquiv.symm f).obj X = f (of X)

Biadditive invariants

structure TauCeti.ExactK0.RightAdditiveInvariant {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (I : Type u) [CategoryTheory.Category.{v, u} I] (E' : ExactStructure D) (G : Type u_2) [AddCommGroup G] : Type (max (max u u') u_2)

An object-level invariant on an indexing category and an exact category which is invariant under isomorphisms in the first variable and additive on conflations in the second variable. Additivity already makes it invariant under isomorphisms in the second variable (TauCeti.ExactK0.RightAdditiveInvariant.map_iso₂).

• obj : I → D → G

  The value of the invariant on a pair of objects.

• map_iso₁ {X X' : I} : ∀ (a : X ≅ X') (Y : D), self.obj X Y = self.obj X' Y

  Isomorphic objects in the first variable receive equal values.

• map_conflation₂ (X : I) {S : CategoryTheory.ShortComplex D} : E'.Conflation S → self.obj X S.X₂ = self.obj X S.X₁ + self.obj X S.X₃

  The invariant is additive on conflations in the second variable.

theorem TauCeti.ExactK0.RightAdditiveInvariant.ext {D : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} D} {inst✝¹ : CategoryTheory.Preadditive D} {inst✝² : CategoryTheory.Limits.HasZeroObject D} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts D} {I : Type u} {inst✝⁴ : CategoryTheory.Category.{v, u} I} {E' : ExactStructure D} {G : Type u_2} {inst✝⁵ : AddCommGroup G} {x y : RightAdditiveInvariant I E' G} (obj : x.obj = y.obj) : x = y

theorem TauCeti.ExactK0.RightAdditiveInvariant.ext_iff {D : Type u'} {inst✝ : CategoryTheory.Category.{v', u'} D} {inst✝¹ : CategoryTheory.Preadditive D} {inst✝² : CategoryTheory.Limits.HasZeroObject D} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts D} {I : Type u} {inst✝⁴ : CategoryTheory.Category.{v, u} I} {E' : ExactStructure D} {G : Type u_2} {inst✝⁵ : AddCommGroup G} {x y : RightAdditiveInvariant I E' G} : x = y ↔ x.obj = y.obj

theorem TauCeti.ExactK0.RightAdditiveInvariant.map_iso₂ {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] {I : Type u} [CategoryTheory.Category.{v, u} I] (a : RightAdditiveInvariant I E' G) (X : I) {Y Y' : D} (e : Y ≅ Y') : a.obj X Y = a.obj X Y'

A right-additive invariant takes equal values on isomorphic objects in its second variable, since it is additive on conflations there.

noncomputable def TauCeti.ExactK0.RightAdditiveInvariant.rightLift {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] {I : Type u} [CategoryTheory.Category.{v, u} I] (a : RightAdditiveInvariant I E' G) (X : I) : ExactK0 E' →+ G

A right-additive invariant with its first argument fixed, descended through the exact Grothendieck group in its second variable.

Equations

• a.rightLift X = TauCeti.ExactK0.lift (TauCeti.ExactK0.RightAdditiveInvariant.additiveInvariant✝ a X)

@[simp]

theorem TauCeti.ExactK0.RightAdditiveInvariant.rightLift_of {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] {I : Type u} [CategoryTheory.Category.{v, u} I] (a : RightAdditiveInvariant I E' G) (X : I) (Y : D) : (a.rightLift X) (of Y) = a.obj X Y

Evaluation of the one-sided descent on an object class.

theorem TauCeti.ExactK0.RightAdditiveInvariant.rightLift_unique {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] {I : Type u} [CategoryTheory.Category.{v, u} I] (a : RightAdditiveInvariant I E' G) (X : I) (f : ExactK0 E' →+ G) (hf : ∀ (Y : D), f (of Y) = a.obj X Y) : f = a.rightLift X

Any homomorphism agreeing with the invariant on the object classes of the second variable is its one-sided descent.

theorem TauCeti.ExactK0.RightAdditiveInvariant.rightLift_congr {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] {I : Type u} [CategoryTheory.Category.{v, u} I] (a : RightAdditiveInvariant I E' G) {X X' : I} (i : X ≅ X') : a.rightLift X = a.rightLift X'

Isomorphic indexing objects induce the same one-sided descent.

structure TauCeti.ExactK0.BiadditiveInvariant {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (G : Type u_2) [AddCommGroup G] extends TauCeti.ExactK0.RightAdditiveInvariant C E' G : Type (max (max u u') u_2)

An object-level invariant on two exact categories which is invariant under isomorphisms and additive on conflations in each variable.

• obj : C → D → G
• map_iso₁ {X X' : C} : ∀ (a : X ≅ X') (Y : D), self.obj X Y = self.obj X' Y
• map_conflation₂ (X : C) {S : CategoryTheory.ShortComplex D} : E'.Conflation S → self.obj X S.X₂ = self.obj X S.X₁ + self.obj X S.X₃
• map_conflation₁ {S : CategoryTheory.ShortComplex C} : E.Conflation S → ∀ (Y : D), self.obj S.X₂ Y = self.obj S.X₁ Y + self.obj S.X₃ Y

  The invariant is additive on conflations in the first variable.

theorem TauCeti.ExactK0.BiadditiveInvariant.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts C} {D : Type u'} {inst✝⁴ : CategoryTheory.Category.{v', u'} D} {inst✝⁵ : CategoryTheory.Preadditive D} {inst✝⁶ : CategoryTheory.Limits.HasZeroObject D} {inst✝⁷ : CategoryTheory.Limits.HasBinaryBiproducts D} {E : ExactStructure C} {E' : ExactStructure D} {G : Type u_2} {inst✝⁸ : AddCommGroup G} {x y : BiadditiveInvariant E E' G} (obj : x.obj = y.obj) : x = y

theorem TauCeti.ExactK0.BiadditiveInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts C} {D : Type u'} {inst✝⁴ : CategoryTheory.Category.{v', u'} D} {inst✝⁵ : CategoryTheory.Preadditive D} {inst✝⁶ : CategoryTheory.Limits.HasZeroObject D} {inst✝⁷ : CategoryTheory.Limits.HasBinaryBiproducts D} {E : ExactStructure C} {E' : ExactStructure D} {G : Type u_2} {inst✝⁸ : AddCommGroup G} {x y : BiadditiveInvariant E E' G} : x = y ↔ x.obj = y.obj

noncomputable def TauCeti.ExactK0.BiadditiveInvariant.bilift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] (a : BiadditiveInvariant E E' G) : ExactK0 E →+ ExactK0 E' →+ G

Descend an object-level biadditive invariant through both exact Grothendieck groups.

Equations

• a.bilift = TauCeti.ExactK0.lift (TauCeti.ExactK0.BiadditiveInvariant.leftInvariant✝ a)

@[simp]

theorem TauCeti.ExactK0.BiadditiveInvariant.bilift_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] (a : BiadditiveInvariant E E' G) (X : C) : a.bilift (of X) = a.rightLift X

The two-variable descent at an object class of the first variable is the one-sided descent in the second variable.

theorem TauCeti.ExactK0.BiadditiveInvariant.bilift_of_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] (a : BiadditiveInvariant E E' G) (X : C) (Y : D) : (a.bilift (of X)) (of Y) = a.obj X Y

The two-variable descent evaluates on object classes as the original invariant.

theorem TauCeti.ExactK0.BiadditiveInvariant.bilift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} {G : Type u_1} [AddCommGroup G] (a : BiadditiveInvariant E E' G) (b : ExactK0 E →+ ExactK0 E' →+ G) (hb : ∀ (X : C) (Y : D), (b (of X)) (of Y) = a.obj X Y) : b = a.bilift

The two-variable descent is the unique biadditive map with the prescribed values on pairs of object classes.

noncomputable def TauCeti.ExactK0.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) : ExactK0 E →+ ExactK0 E'

Functoriality of exact K₀: a conflation-exact functor induces a homomorphism of exact Grothendieck groups.

Equations

• TauCeti.ExactK0.map F hF = TauCeti.PresentedK0.map F ⋯

@[simp]

theorem TauCeti.ExactK0.map_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) (X : C) : (map F hF) (of X) = of (F.obj X)

theorem TauCeti.ExactK0.map_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) (f : ExactK0 E →+ ExactK0 E') (hf : ∀ (X : C), f (of X) = of (F.obj X)) : f = map F hF

Any homomorphism sending object classes to the classes of their images is the induced map.

@[simp]

theorem TauCeti.ExactK0.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : ExactStructure C) : map (CategoryTheory.Functor.id C) ⋯ = AddMonoidHom.id (ExactK0 E)

The identity functor induces the identity of exact K₀.

theorem TauCeti.ExactK0.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (F : CategoryTheory.Functor C D) [F.Additive] {K : Type u''} [CategoryTheory.Category.{v'', u''} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] [CategoryTheory.EssentiallySmall.{w'', v'', u''} K] {E'' : ExactStructure K} (H : CategoryTheory.Functor D K) [H.Additive] (hF : E.IsConflationExact E' F) (hH : E'.IsConflationExact E'' H) : map (F.comp H) ⋯ = (map H hH).comp (map F hF)

The induced maps of a composite of conflation-exact functors compose.

theorem TauCeti.ExactK0.map_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (F : CategoryTheory.Functor C D) [F.Additive] {F' : CategoryTheory.Functor C D} [F'.Additive] (h : ∀ (X : C), Nonempty (F.obj X ≅ F'.obj X)) (hF : E.IsConflationExact E' F) (hF' : E.IsConflationExact E' F') : map F hF = map F' hF'

Conflation-exact functors with isomorphic values on every object induce the same map.

noncomputable def TauCeti.ExactK0.mapEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (e : C ≌ D) [e.functor.Additive] (hF : E.IsConflationExact E' e.functor) (hG : E'.IsConflationExact E e.inverse) : ExactK0 E ≃+ ExactK0 E'

Equivalence invariance of exact K₀: an exact equivalence, that is an equivalence whose two functors are conflation-exact, induces an isomorphism of exact Grothendieck groups.

Equations

• TauCeti.ExactK0.mapEquiv e hF hG = TauCeti.PresentedK0.mapEquiv e ⋯ ⋯

@[simp]

theorem TauCeti.ExactK0.mapEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (e : C ≌ D) [e.functor.Additive] (hF : E.IsConflationExact E' e.functor) (hG : E'.IsConflationExact E e.inverse) (X : C) : (mapEquiv e hF hG) (of X) = of (e.functor.obj X)

@[simp]

theorem TauCeti.ExactK0.mapEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (e : C ≌ D) [e.functor.Additive] (hF : E.IsConflationExact E' e.functor) (hG : E'.IsConflationExact E e.inverse) (Y : D) : (mapEquiv e hF hG).symm (of Y) = of (e.inverse.obj Y)

noncomputable def TauCeti.ExactK0.transportEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] : ExactK0 E ≃+ ExactK0 (E.transport e)

Transporting an exact structure along an additive equivalence does not change its exact K₀.

Equations

• TauCeti.ExactK0.transportEquiv E e = TauCeti.ExactK0.mapEquiv e ⋯ ⋯

@[simp]

theorem TauCeti.ExactK0.transportEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] (X : C) : (transportEquiv E e) (of X) = of (e.functor.obj X)

noncomputable def TauCeti.ExactK0.ofLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S → E''.Conflation S) : ExactK0 E →+ ExactK0 E''

The comparison map of two exact structures: enlarging the class of conflations imposes more relations, and the identity functor induces a homomorphism of exact Grothendieck groups.

Equations

• TauCeti.ExactK0.ofLE h = TauCeti.PresentedK0.ofLE ⋯

@[simp]

theorem TauCeti.ExactK0.ofLE_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S → E''.Conflation S) (X : C) : (ofLE h) (of X) = of X

noncomputable def TauCeti.ExactK0.ofLEEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S ↔ E''.Conflation S) : ExactK0 E ≃+ ExactK0 E''

The comparison isomorphism between two exact structures with the same conflations: the comparison maps TauCeti.ExactK0.ofLE in both directions are mutually inverse.

Equations

• TauCeti.ExactK0.ofLEEquiv h = (TauCeti.ExactK0.ofLE ⋯).toAddEquiv (TauCeti.ExactK0.ofLE ⋯) ⋯ ⋯

@[simp]

theorem TauCeti.ExactK0.ofLEEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S ↔ E''.Conflation S) (X : C) : (ofLEEquiv h) (of X) = of X

@[simp]

theorem TauCeti.ExactK0.ofLEEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S ↔ E''.Conflation S) (X : C) : (ofLEEquiv h).symm (of X) = of X

theorem TauCeti.ExactK0.ofLE_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S → E''.Conflation S) (f : ExactK0 E →+ ExactK0 E'') (hf : ∀ (X : C), f (of X) = of X) : f = ofLE h

The universal characterization of the comparison map: it is the unique homomorphism preserving the classes of objects.

theorem TauCeti.ExactK0.ofLE_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S → E''.Conflation S) : Function.Surjective ⇑(ofLE h)

The comparison map is surjective: exact K₀ is a quotient of the exact K₀ of any exact structure with fewer conflations.

@[simp]

theorem TauCeti.ExactK0.ofLE_refl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} : ofLE ⋯ = AddMonoidHom.id (ExactK0 E)

The comparison map of an exact structure with itself is the identity.

theorem TauCeti.ExactK0.ofLE_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E E'' E₃ : ExactStructure C} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S → E''.Conflation S) (h' : ∀ (S : CategoryTheory.ShortComplex C), E''.Conflation S → E₃.Conflation S) : (ofLE h').comp (ofLE h) = ofLE ⋯

Comparison maps for successive enlargements of the class of conflations compose.

theorem TauCeti.ExactK0.map_comp_ofLE {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E E'' : ExactStructure C} {E₁' E₂' : ExactStructure D} (h : ∀ (S : CategoryTheory.ShortComplex C), E.Conflation S → E''.Conflation S) (h' : ∀ (S : CategoryTheory.ShortComplex D), E₁'.Conflation S → E₂'.Conflation S) (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E₁' F) (hF' : E''.IsConflationExact E₂' F) : (map F hF').comp (ofLE h) = (ofLE h').comp (map F hF)

Naturality of the comparison map in a functor which is conflation-exact for both pairs of exact structures.

noncomputable def TauCeti.ExactK0.fromSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : ExactStructure C) : SplitK0 C →+ ExactK0 E

The canonical comparison from split K₀ to exact K₀. It is induced by the class map, which respects biproduct relations because every exact structure contains the biproduct conflations.

Equations

• TauCeti.ExactK0.fromSplit E = TauCeti.SplitK0.lift { obj := fun (X : C) => TauCeti.ExactK0.of X, map_iso := ⋯, map_biprod := ⋯ }

@[simp]

theorem TauCeti.ExactK0.fromSplit_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} (X : C) : (fromSplit E) (SplitK0.of X) = of X

theorem TauCeti.ExactK0.fromSplit_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} (f : SplitK0 C →+ ExactK0 E) (hf : ∀ (X : C), f (SplitK0.of X) = of X) : f = fromSplit E

The canonical comparison out of split K₀ is the unique homomorphism preserving the classes of objects.

theorem TauCeti.ExactK0.fromSplit_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} : Function.Surjective ⇑(fromSplit E)

The canonical comparison out of split K₀ is surjective: the classes of objects generate exact K₀, so the exact K₀ of any exact structure is a quotient of split K₀.

noncomputable def TauCeti.ExactK0.fromSplitEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} (h : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → Nonempty S.Splitting) : SplitK0 C ≃+ ExactK0 E

The canonical comparison from split K₀ to exact K₀ is an equivalence when every conflation splits.

Equations

• TauCeti.ExactK0.fromSplitEquiv h = (TauCeti.ExactK0.fromSplit E).toAddEquiv (TauCeti.ExactK0.lift { obj := TauCeti.SplitK0.of, map_conflation := ⋯ }) ⋯ ⋯

@[simp]

theorem TauCeti.ExactK0.fromSplitEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} (h : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → Nonempty S.Splitting) (x : SplitK0 C) : (fromSplitEquiv ⋯) x = (fromSplit E) x

The split-to-exact equivalence acts by the canonical comparison homomorphism.

@[simp]

theorem TauCeti.ExactK0.fromSplitEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {E : ExactStructure C} (h : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → Nonempty S.Splitting) (X : C) : (fromSplitEquiv ⋯).symm (of X) = SplitK0.of X

The inverse split-to-exact equivalence sends an object class to its split class.

theorem TauCeti.ExactK0.map_comp_fromSplit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E : ExactStructure C} {E' : ExactStructure D} (F : CategoryTheory.Functor C D) [F.Additive] (hF : E.IsConflationExact E' F) : (map F hF).comp (fromSplit E) = (fromSplit E').comp (SplitK0.map F)

The canonical comparison out of split K₀ is natural in a conflation-exact functor: every additive functor is conflation-exact for the split exact structures.