Grothendieck presentations

This file owns the algebraic quotient used by the repository's triangulated Grothendieck group. A presentation consists of generators and three-term relations middle = left + right; its group is the free abelian group on the generators modulo those relations.

structure CategoryTheory.GrothendieckPresentation (Generator : Type u) (Relation : Type v) : Type (max u v)

A presentation by three-term additive relations.

• left : Relation → Generator

  The left term of a relation.

• middle : Relation → Generator

  The middle term of a relation.

• right : Relation → Generator

  The right term of a relation.

def CategoryTheory.GrothendieckPresentation.relationSubgroup {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) : AddSubgroup (FreeAbelianGroup Generator)

The subgroup generated by the relation elements [middle] - [left] - [right].

Equations

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

@[reducible, inline]

abbrev CategoryTheory.GrothendieckPresentation.Group {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) : Type u

The abelian group presented by P.

Equations

• P.Group = (FreeAbelianGroup Generator ⧸ P.relationSubgroup)

@[implicit_reducible]

instance CategoryTheory.GrothendieckPresentation.instAddCommGroupGroup {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) : AddCommGroup P.Group

Equations

• P.instAddCommGroupGroup = { toAddGroup := QuotientAddGroup.Quotient.addGroup P.relationSubgroup, add_comm := ⋯ }

def CategoryTheory.GrothendieckPresentation.of {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) (X : Generator) : P.Group

The class of a generator in the presented group.

Equations

• P.of X = ↑(FreeAbelianGroup.of X)

theorem CategoryTheory.GrothendieckPresentation.of_relation {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) (r : Relation) : P.of (P.middle r) = P.of (P.left r) + P.of (P.right r)

The defining three-term relation in the presented group.

class CategoryTheory.GrothendieckPresentation.IsAdditive {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {A : Type u_1} [AddCommGroup A] (f : Generator → A) : Prop

A function respects a Grothendieck presentation when it sends every three-term relation to an additive equality.

• additive (r : Relation) : f (P.middle r) = f (P.left r) + f (P.right r)

def CategoryTheory.GrothendieckPresentation.lift {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {A : Type u_1} [AddCommGroup A] (f : Generator → A) [P.IsAdditive f] : P.Group →+ A

The universal additive map out of a Grothendieck presentation.

Equations

• P.lift f = QuotientAddGroup.lift P.relationSubgroup (FreeAbelianGroup.lift f) ⋯

@[simp]

theorem CategoryTheory.GrothendieckPresentation.lift_of {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {A : Type u_1} [AddCommGroup A] (f : Generator → A) [P.IsAdditive f] (X : Generator) : (P.lift f) (P.of X) = f X

theorem CategoryTheory.GrothendieckPresentation.hom_ext {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {A : Type u_1} [AddCommGroup A] {f g : P.Group →+ A} (h : ∀ (X : Generator), f (P.of X) = g (P.of X)) : f = g

Additive maps out of the presented group are determined by generator classes.

theorem CategoryTheory.GrothendieckPresentation.hom_ext_iff {Generator : Type u} {Relation : Type v} {P : GrothendieckPresentation Generator Relation} {A : Type u_1} [AddCommGroup A] {f g : P.Group →+ A} : f = g ↔ ∀ (X : Generator), f (P.of X) = g (P.of X)

theorem CategoryTheory.GrothendieckPresentation.induction_on {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {motive : P.Group → Prop} (x : P.Group) (of : ∀ (X : Generator), motive (P.of X)) (zero : motive 0) (neg : ∀ (a : P.Group), motive a → motive (-a)) (add : ∀ (a b : P.Group), motive a → motive b → motive (a + b)) : motive x

Induction on a presented Grothendieck group through generators and the abelian-group operations.

instance CategoryTheory.GrothendieckPresentation.isAdditive_of {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) : P.IsAdditive P.of

def CategoryTheory.GrothendieckPresentation.map {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {Generator' : Type u'} {Relation' : Type v'} {Q : GrothendieckPresentation Generator' Relation'} (f : Generator → Generator') (hf : P.IsAdditive (Q.of ∘ f)) : P.Group →+ Q.Group

A generator map respecting relations induces a homomorphism of presented Grothendieck groups.

Equations

• P.map f hf = P.lift (Q.of ∘ f)

@[simp]

theorem CategoryTheory.GrothendieckPresentation.map_of {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {Generator' : Type u'} {Relation' : Type v'} {Q : GrothendieckPresentation Generator' Relation'} (f : Generator → Generator') (hf : P.IsAdditive (Q.of ∘ f)) (X : Generator) : (P.map f hf) (P.of X) = Q.of (f X)

theorem CategoryTheory.GrothendieckPresentation.IsAdditive.of_relationMap {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) {Generator' : Type u'} {Relation' : Type v'} {Q : GrothendieckPresentation Generator' Relation'} (fGenerator : Generator → Generator') (fRelation : Relation → Relation') (hleft : ∀ (r : Relation), fGenerator (P.left r) = Q.left (fRelation r)) (hmiddle : ∀ (r : Relation), fGenerator (P.middle r) = Q.middle (fRelation r)) (hright : ∀ (r : Relation), fGenerator (P.right r) = Q.right (fRelation r)) : P.IsAdditive (Q.of ∘ fGenerator)

A compatible relation map proves that the generator map is additive.

theorem CategoryTheory.GrothendieckPresentation.map_id {Generator : Type u} {Relation : Type v} (P : GrothendieckPresentation Generator Relation) : P.map id ⋯ = AddMonoidHom.id P.Group

theorem CategoryTheory.GrothendieckPresentation.map_comp {Generator : Type u} {Relation : Type v} {P : GrothendieckPresentation Generator Relation} {Generator' : Type u'} {Relation' : Type v'} {Q : GrothendieckPresentation Generator' Relation'} {Generator'' : Type u''} {Relation'' : Type v''} {R : GrothendieckPresentation Generator'' Relation''} (f : Generator → Generator') (g : Generator' → Generator'') (hf : P.IsAdditive (Q.of ∘ f)) (hg : Q.IsAdditive (R.of ∘ g)) (hgf : P.IsAdditive (R.of ∘ g ∘ f)) : P.map (g ∘ f) hgf = (Q.map g hg).comp (P.map f hf)

Composition law for maps of Grothendieck presentations.