Choice independence of the small presentation of K₀

A categorical Grothendieck group is a quotient of a free abelian group whose generators index the isomorphism classes of objects. TauCeti.PresentedK0 takes those generators to be TauCeti.ObjectCode C = Shrink (Skeleton C), but this is only one small type in bijection with the isomorphism classes: the skeleton of Mathlib's chosen small model SmallModel C, or the codes ObjectCode C formed in another universe, serve as well. This file shows that the choice does not matter, canonically.

A model m : TauCeti.IsoClassModel C I of the isomorphism classes of C is a surjective map m.code : C → I under which two objects have the same code exactly when they are isomorphic. Relations are given at the level of objects, as a set ρ of integral combinations of objects, so that they make sense over every model at once, and m.K0 ρ is the free abelian group on I modulo the codes of the relations. Over two models m and m' the groups m.K0 ρ and m'.K0 ρ are related by a canonical isomorphism TauCeti.IsoClassModel.K0.equiv m m' ρ, the unique homomorphism sending the class of each object to its class. These isomorphisms satisfy the cocycle laws, and they commute with the maps induced by functors. The public group TauCeti.PresentedK0 of the codes of ρ is identified with m.K0 ρ for every model m by TauCeti.IsoClassModel.K0.presentedK0Equiv, compatibly with these isomorphisms.

Main definitions

• TauCeti.IsoClassModel C I: a model of the isomorphism classes of objects of C in I, with the instances TauCeti.IsoClassModel.objectCode, TauCeti.IsoClassModel.skeleton and TauCeti.IsoClassModel.smallModel, and the transports TauCeti.IsoClassModel.ofEquiv and TauCeti.IsoClassModel.ofEquivalence.
• TauCeti.IsoClassModel.equiv m m': the bijection between the index types of two models which sends the code of an object to its code.
• TauCeti.IsoClassModel.K0 m ρ: the Grothendieck group presented by the object-level relations ρ over the model m, with its class map TauCeti.IsoClassModel.K0.of, its universal property TauCeti.IsoClassModel.K0.lift and its functoriality TauCeti.IsoClassModel.K0.map.
• TauCeti.IsoClassModel.K0.equiv m m' ρ: the canonical isomorphism m.K0 ρ ≃+ m'.K0 ρ.
• TauCeti.IsoClassModel.K0.presentedK0Equiv m ρ: the canonical isomorphism from the public presentation TauCeti.PresentedK0 of the codes of ρ to m.K0 ρ.

Main results

• TauCeti.IsoClassModel.K0.equiv_of and TauCeti.IsoClassModel.K0.equiv_unique: the canonical isomorphism preserves the class of every object, and is the only homomorphism doing so.
• TauCeti.IsoClassModel.K0.equiv_refl, TauCeti.IsoClassModel.K0.equiv_symm and TauCeti.IsoClassModel.K0.equiv_trans: the cocycle laws.
• TauCeti.IsoClassModel.K0.equiv_map: naturality of the canonical isomorphisms with respect to the maps induced by functors.
• TauCeti.IsoClassModel.K0.presentedK0Equiv_trans_equiv: the identification with the public presentation is compatible with the canonical isomorphisms.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 6, where K₀ of an essentially small category is presented on a set of representatives of the isomorphism classes, and the universal property of an additive invariant removes the dependence on that set.

structure TauCeti.IsoClassModel (C : Type u) [CategoryTheory.Category.{v, u} C] (I : Type w) : Type (max u w)

A model of the isomorphism classes of objects of C in a type I: a surjective map from the objects of C to I under which two objects have the same image exactly when they are isomorphic.

• code : C → I

  The element of I coding the isomorphism class of an object.

• code_surjective : Function.Surjective self.code

  Every element of I codes some object.

• code_eq_code_iff {X Y : C} : self.code X = self.code Y ↔ Nonempty (X ≅ Y)

  Two objects have the same code exactly when they are isomorphic.

theorem TauCeti.IsoClassModel.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {I : Type w} {x y : IsoClassModel C I} (code : x.code = y.code) : x = y

theorem TauCeti.IsoClassModel.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {I : Type w} {x y : IsoClassModel C I} : x = y ↔ x.code = y.code

theorem TauCeti.IsoClassModel.code_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} (m : IsoClassModel C I) {X Y : C} (e : X ≅ Y) : m.code X = m.code Y

def TauCeti.IsoClassModel.skeleton (C : Type u) [CategoryTheory.Category.{v, u} C] : IsoClassModel C (CategoryTheory.Skeleton C)

The isomorphism classes of C modelled by the objects of its skeleton.

Equations

• TauCeti.IsoClassModel.skeleton C = { code := CategoryTheory.toSkeleton, code_surjective := ⋯, code_eq_code_iff := ⋯ }

noncomputable def TauCeti.IsoClassModel.objectCode (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : IsoClassModel C (ObjectCode C)

The model underlying TauCeti.PresentedK0: the codes TauCeti.ObjectCode C.

Equations

• TauCeti.IsoClassModel.objectCode C = { code := TauCeti.objectCode, code_surjective := ⋯, code_eq_code_iff := ⋯ }

def TauCeti.IsoClassModel.ofEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) (e : I ≃ J) : IsoClassModel C J

A model transported along a bijection of its index type.

Equations

• m.ofEquiv e = { code := fun (X : C) => e (m.code X), code_surjective := ⋯, code_eq_code_iff := ⋯ }

def TauCeti.IsoClassModel.ofEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {D : Type u'} [CategoryTheory.Category.{v', u'} D] (m : IsoClassModel D I) (e : C ≌ D) : IsoClassModel C I

A model of the isomorphism classes of D pulled back along an equivalence C ≌ D.

Equations

• m.ofEquivalence e = { code := fun (X : C) => m.code (e.functor.obj X), code_surjective := ⋯, code_eq_code_iff := ⋯ }

noncomputable def TauCeti.IsoClassModel.smallModel (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] : IsoClassModel C (CategoryTheory.Skeleton (CategoryTheory.SmallModel.{w, v, u} C))

The isomorphism classes of C modelled by the skeleton of Mathlib's chosen small model SmallModel C.

Equations

• TauCeti.IsoClassModel.smallModel C = (TauCeti.IsoClassModel.skeleton (CategoryTheory.SmallModel.{?u.3, ?u.2, ?u.1} C)).ofEquivalence (CategoryTheory.equivSmallModel C)

@[simp]

theorem TauCeti.IsoClassModel.skeleton_code {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (skeleton C).code X = CategoryTheory.toSkeleton X

@[simp]

theorem TauCeti.IsoClassModel.objectCode_code {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (objectCode C).code X = TauCeti.objectCode X

@[simp]

theorem TauCeti.IsoClassModel.ofEquiv_code {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) (e : I ≃ J) (X : C) : (m.ofEquiv e).code X = e (m.code X)

@[simp]

theorem TauCeti.IsoClassModel.ofEquivalence_code {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {D : Type u'} [CategoryTheory.Category.{v', u'} D] (m : IsoClassModel D I) (e : C ≌ D) (X : C) : (m.ofEquivalence e).code X = m.code (e.functor.obj X)

@[simp]

theorem TauCeti.IsoClassModel.smallModel_code {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (X : C) : (smallModel C).code X = CategoryTheory.toSkeleton ((CategoryTheory.equivSmallModel C).functor.obj X)

noncomputable def TauCeti.IsoClassModel.equiv {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) (m' : IsoClassModel C J) : I ≃ J

The bijection between the index types of two models of the isomorphism classes of C which sends the code of an object in the first model to its code in the second.

Equations

• m.equiv m' = { toFun := fun (i : I) => m'.code (Function.surjInv ⋯ i), invFun := fun (j : J) => m.code (Function.surjInv ⋯ j), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.IsoClassModel.equiv_code {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) (m' : IsoClassModel C J) (X : C) : (m.equiv m') (m.code X) = m'.code X

theorem TauCeti.IsoClassModel.equiv_unique {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) (m' : IsoClassModel C J) (f : I → J) (hf : ∀ (X : C), f (m.code X) = m'.code X) : ⇑(m.equiv m') = f

The bijection between two models is the only map compatible with the codes.

@[simp]

theorem TauCeti.IsoClassModel.equiv_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} (m : IsoClassModel C I) : m.equiv m = Equiv.refl I

@[simp]

theorem TauCeti.IsoClassModel.equiv_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) (m' : IsoClassModel C J) : (m.equiv m').symm = m'.equiv m

@[simp]

theorem TauCeti.IsoClassModel.equiv_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {K : Type w''} (m : IsoClassModel C I) (m' : IsoClassModel C J) (m'' : IsoClassModel C K) : (m.equiv m').trans (m'.equiv m'') = m.equiv m''

def TauCeti.IsoClassModel.K0 {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} (m : IsoClassModel C I) (ρ : Set (FreeAbelianGroup C)) : Type w

The Grothendieck group presented by the object-level relations ρ over the model m: the free abelian group on I modulo the subgroup generated by the codes of the relations.

Equations

• m.K0 ρ = (FreeAbelianGroup I ⧸ AddSubgroup.closure (⇑(FreeAbelianGroup.map m.code) '' ρ))

@[instance_reducible]

instance TauCeti.IsoClassModel.instAddCommGroupK0 {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} (m : IsoClassModel C I) (ρ : Set (FreeAbelianGroup C)) : AddCommGroup (m.K0 ρ)

Equations

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

def TauCeti.IsoClassModel.K0.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} : FreeAbelianGroup I →+ m.K0 ρ

The quotient map presenting TauCeti.IsoClassModel.K0 m ρ.

Equations

• TauCeti.IsoClassModel.K0.mk = QuotientAddGroup.mk' (AddSubgroup.closure (⇑(FreeAbelianGroup.map m.code) '' ρ))

theorem TauCeti.IsoClassModel.K0.mk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} : Function.Surjective ⇑mk

theorem TauCeti.IsoClassModel.K0.mk_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (r : FreeAbelianGroup I) : mk r = 0 ↔ r ∈ AddSubgroup.closure (⇑(FreeAbelianGroup.map m.code) '' ρ)

noncomputable def TauCeti.IsoClassModel.K0.of {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (X : C) : m.K0 ρ

The class of an object of C.

Equations

• TauCeti.IsoClassModel.K0.of X = TauCeti.IsoClassModel.K0.mk (FreeAbelianGroup.of (m.code X))

@[simp]

theorem TauCeti.IsoClassModel.K0.mk_of_code {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (X : C) : mk (FreeAbelianGroup.of (m.code X)) = of X

theorem TauCeti.IsoClassModel.K0.of_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {X Y : C} (e : X ≅ Y) : of X = of Y

theorem TauCeti.IsoClassModel.K0.mk_map_code {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (r : FreeAbelianGroup C) : mk ((FreeAbelianGroup.map m.code) r) = (FreeAbelianGroup.lift of) r

The class map, extended additively to integral combinations of objects, is the quotient map applied to their codes.

theorem TauCeti.IsoClassModel.K0.lift_of_eq_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {r : FreeAbelianGroup C} (hr : r ∈ AddSubgroup.closure ρ) : (FreeAbelianGroup.lift of) r = 0

The class map satisfies every relation in the subgroup generated by ρ.

theorem TauCeti.IsoClassModel.K0.closure_range_of {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} : AddSubgroup.closure (Set.range of) = ⊤

The classes of objects generate the presented Grothendieck group.

theorem TauCeti.IsoClassModel.K0.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {G : Type u_1} [AddMonoid G] {f g : m.K0 ρ →+ G} (h : ∀ (X : C), f (of X) = g (of X)) : f = g

Two homomorphisms out of m.K0 ρ agreeing on the classes of objects are equal.

theorem TauCeti.IsoClassModel.K0.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {G : Type u_1} [AddMonoid G] {f g : m.K0 ρ →+ G} : f = g ↔ ∀ (X : C), f (of X) = g (of X)

noncomputable def TauCeti.IsoClassModel.K0.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {G : Type u_1} [AddCommGroup G] (f : C → G) (hf : ∀ ⦃X Y : C⦄ (a : X ≅ Y), f X = f Y) (hρ : ∀ r ∈ ρ, (FreeAbelianGroup.lift f) r = 0) : m.K0 ρ →+ G

The universal property: an isomorphism-invariant function on objects whose additive extension annihilates every relation induces a homomorphism out of m.K0 ρ.

Equations

• TauCeti.IsoClassModel.K0.lift f hf hρ = QuotientAddGroup.lift (AddSubgroup.closure (⇑(FreeAbelianGroup.map m.code) '' ρ)) (FreeAbelianGroup.lift (f ∘ Function.surjInv ⋯)) ⋯

@[simp]

theorem TauCeti.IsoClassModel.K0.lift_of {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {G : Type u_1} [AddCommGroup G] (f : C → G) (hf : ∀ ⦃X Y : C⦄ (a : X ≅ Y), f X = f Y) (hρ : ∀ r ∈ ρ, (FreeAbelianGroup.lift f) r = 0) (X : C) : (lift f hf hρ) (of X) = f X

theorem TauCeti.IsoClassModel.K0.lift_unique {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {G : Type u_1} [AddCommGroup G] (f : C → G) (hf : ∀ ⦃X Y : C⦄ (a : X ≅ Y), f X = f Y) (hρ : ∀ r ∈ ρ, (FreeAbelianGroup.lift f) r = 0) (g : m.K0 ρ →+ G) (hg : ∀ (X : C), g (of X) = f X) : g = lift f hf hρ

noncomputable def TauCeti.IsoClassModel.K0.map {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) {ρ : Set (FreeAbelianGroup C)} {D : Type u'} [CategoryTheory.Category.{v', u'} D] {σ : Set (FreeAbelianGroup D)} (n : IsoClassModel D J) (F : CategoryTheory.Functor C D) (h : ∀ r ∈ ρ, (FreeAbelianGroup.map F.obj) r ∈ AddSubgroup.closure σ) : m.K0 ρ →+ n.K0 σ

Functoriality: a functor carrying every relation of ρ into the subgroup generated by σ induces a homomorphism between the presented Grothendieck groups, over any two models.

Equations

• TauCeti.IsoClassModel.K0.map m n F h = TauCeti.IsoClassModel.K0.lift (fun (X : C) => TauCeti.IsoClassModel.K0.of (F.obj X)) ⋯ ⋯

@[simp]

theorem TauCeti.IsoClassModel.K0.map_of {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {D : Type u'} [CategoryTheory.Category.{v', u'} D] {σ : Set (FreeAbelianGroup D)} (n : IsoClassModel D J) (F : CategoryTheory.Functor C D) (h : ∀ r ∈ ρ, (FreeAbelianGroup.map F.obj) r ∈ AddSubgroup.closure σ) (X : C) : (map m n F h) (of X) = of (F.obj X)

theorem TauCeti.IsoClassModel.K0.map_comp_mem_closure {C : Type u} [CategoryTheory.Category.{v, u} C] {ρ : Set (FreeAbelianGroup C)} {D : Type u'} [CategoryTheory.Category.{v', u'} D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] {σ : Set (FreeAbelianGroup D)} {τ : Set (FreeAbelianGroup E)} (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (hF : ∀ r ∈ ρ, (FreeAbelianGroup.map F.obj) r ∈ AddSubgroup.closure σ) (hG : ∀ r ∈ σ, (FreeAbelianGroup.map G.obj) r ∈ AddSubgroup.closure τ) (r : FreeAbelianGroup C) : r ∈ ρ → (FreeAbelianGroup.map (F.comp G).obj) r ∈ AddSubgroup.closure τ

A composite functor carries ρ into the subgroup generated by τ when each of its factors carries its relations into the next generated subgroup.

theorem TauCeti.IsoClassModel.K0.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {K : Type w''} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} {D : Type u'} [CategoryTheory.Category.{v', u'} D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] {σ : Set (FreeAbelianGroup D)} {τ : Set (FreeAbelianGroup E)} (n : IsoClassModel D J) (p : IsoClassModel E K) (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) (hF : ∀ r ∈ ρ, (FreeAbelianGroup.map F.obj) r ∈ AddSubgroup.closure σ) (hG : ∀ r ∈ σ, (FreeAbelianGroup.map G.obj) r ∈ AddSubgroup.closure τ) (hFG : ∀ r ∈ ρ, (FreeAbelianGroup.map (F.comp G).obj) r ∈ AddSubgroup.closure τ := ⋯) : map m p (F.comp G) hFG = (map n p G hG).comp (map m n F hF)

noncomputable def TauCeti.IsoClassModel.K0.equiv {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} (m : IsoClassModel C I) (m' : IsoClassModel C J) (ρ : Set (FreeAbelianGroup C)) : m.K0 ρ ≃+ m'.K0 ρ

The canonical isomorphism between the Grothendieck groups presented by the same relations over two models of the isomorphism classes of C. It sends the class of every object to its class; see TauCeti.IsoClassModel.K0.equiv_of and TauCeti.IsoClassModel.K0.equiv_unique.

Equations

• TauCeti.IsoClassModel.K0.equiv m m' ρ = (TauCeti.IsoClassModel.K0.map m m' (CategoryTheory.Functor.id C) ⋯).toAddEquiv (TauCeti.IsoClassModel.K0.map m' m (CategoryTheory.Functor.id C) ⋯) ⋯ ⋯

@[simp]

theorem TauCeti.IsoClassModel.K0.equiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (m' : IsoClassModel C J) (X : C) : (equiv m m' ρ) (of X) = of X

theorem TauCeti.IsoClassModel.K0.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (m' : IsoClassModel C J) (h : ∀ r ∈ ρ, (FreeAbelianGroup.map (CategoryTheory.Functor.id C).obj) r ∈ AddSubgroup.closure ρ) : map m m' (CategoryTheory.Functor.id C) h = ↑(equiv m m' ρ)

The map induced by the identity functor between two models is the canonical isomorphism.

theorem TauCeti.IsoClassModel.K0.equiv_unique {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (m' : IsoClassModel C J) (f : m.K0 ρ →+ m'.K0 ρ) (hf : ∀ (X : C), f (of X) = of X) : f = ↑(equiv m m' ρ)

The canonical isomorphism is the only homomorphism preserving the class of every object.

@[simp]

theorem TauCeti.IsoClassModel.K0.equiv_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} : equiv m m ρ = AddEquiv.refl (m.K0 ρ)

@[simp]

theorem TauCeti.IsoClassModel.K0.equiv_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (m' : IsoClassModel C J) : (equiv m m' ρ).symm = equiv m' m ρ

@[simp]

theorem TauCeti.IsoClassModel.K0.equiv_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {K : Type w''} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (m' : IsoClassModel C J) (m'' : IsoClassModel C K) : (equiv m m' ρ).trans (equiv m' m'' ρ) = equiv m m'' ρ

The cocycle law for the canonical isomorphisms.

theorem TauCeti.IsoClassModel.K0.equiv_map {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} (m' : IsoClassModel C J) {D : Type u'} [CategoryTheory.Category.{v', u'} D] {J' : Type u_1} {K' : Type u_2} {σ : Set (FreeAbelianGroup D)} (n : IsoClassModel D J') (n' : IsoClassModel D K') (F : CategoryTheory.Functor C D) (h : ∀ r ∈ ρ, (FreeAbelianGroup.map F.obj) r ∈ AddSubgroup.closure σ) (x : m.K0 ρ) : (equiv n n' σ) ((map m n F h) x) = (map m' n' F h) ((equiv m m' ρ) x)

Naturality of the canonical isomorphisms: they commute with the maps induced by a functor.

noncomputable def TauCeti.IsoClassModel.K0.presentedK0Equiv {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} (m : IsoClassModel C I) (ρ : Set (FreeAbelianGroup C)) [CategoryTheory.EssentiallySmall.{w', v, u} C] : PresentedK0 (⇑(FreeAbelianGroup.map TauCeti.objectCode) '' ρ) ≃+ m.K0 ρ

The public presentation TauCeti.PresentedK0 of the codes of the object-level relations ρ is canonically isomorphic to the presentation of ρ over any model m, by the isomorphism preserving the class of every object.

Equations

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

@[simp]

theorem TauCeti.IsoClassModel.K0.presentedK0Equiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} [CategoryTheory.EssentiallySmall.{w', v, u} C] (X : C) : (presentedK0Equiv m ρ) (PresentedK0.of X) = of X

@[simp]

theorem TauCeti.IsoClassModel.K0.presentedK0Equiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} [CategoryTheory.EssentiallySmall.{w', v, u} C] (X : C) : (presentedK0Equiv m ρ).symm (of X) = PresentedK0.of X

@[simp]

theorem TauCeti.IsoClassModel.K0.presentedK0Equiv_trans_equiv {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type w} {J : Type w'} {m : IsoClassModel C I} {ρ : Set (FreeAbelianGroup C)} [CategoryTheory.EssentiallySmall.{w', v, u} C] (m' : IsoClassModel C J) : (presentedK0Equiv m ρ).trans (equiv m m' ρ) = presentedK0Equiv m' ρ

The identification with the public presentation is compatible with the canonical isomorphisms between models.