The product of two dg categories

Objects are pairs, and the Hom-complex between two pairs is the degreewise product of the two Hom-complexes, with componentwise differential, identity and composition.

Unlike the opposite, no sign enters: the product is a limit construction and every axiom holds componentwise. The work is entirely in getting Lean to see the Hom-objects as products. AddCommGrpCat.of (_ × _)'s carrier is opaque to instance search, so two techniques carry the file:

• Build at plain types. prodComp is stated for arbitrary AddCommGroups and then applied to the carriers. Term elaboration unifies up to defeq, so this works where instance search does not.
• Restate the projection lemmas where simp will match them. Prod.fst_add does not fire on (dgHom X Y).X p, because the operation carries the carrier's instance rather than Prod's. The rfl lemmas below say the same thing at the type the goals actually have — and the type has to be exactly that one, not the prodComplex it unfolds to.

def CategoryTheory.prodD (K L : CochainComplex AddCommGrpCat ℤ) (p q : ℤ) : AddCommGrpCat.of (↑(K.X p) × ↑(L.X p)) ⟶ AddCommGrpCat.of (↑(K.X q) × ↑(L.X q))

The differential of the degreewise product, named separately: a proof in a later field of a structure instance cannot see an earlier field given inline, so d has to exist before shape and d_comp_d' can mention it.

Equations

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

def CategoryTheory.prodComplex (K L : CochainComplex AddCommGrpCat ℤ) : CochainComplex AddCommGrpCat ℤ

The degreewise product of two cochain complexes of abelian groups.

Equations

• CategoryTheory.prodComplex K L = { X := fun (p : ℤ) => AddCommGrpCat.of (↑(K.X p) × ↑(L.X p)), d := CategoryTheory.prodD K L, shape := ⋯, d_comp_d' := ⋯ }

@[simp]

theorem CategoryTheory.prodComplex_X_coe (K L : CochainComplex AddCommGrpCat ℤ) (p : ℤ) : ↑((prodComplex K L).X p) = (↑(K.X p) × ↑(L.X p))

@[simp]

theorem CategoryTheory.prodComplex_d (K L : CochainComplex AddCommGrpCat ℤ) (p q : ℤ) : (prodComplex K L).d p q = prodD K L p q

Building the instance at plain types

The obstacle the first attempt hit is that ((prodComplex K L).X p) is AddCommGrpCat.of (_ × _), whose carrier instance search will not see through. Term elaboration is a different matter: it unifies up to defeq, so a helper stated at plain types with AddCommGroup instances applies to those carriers without complaint.

So the composition is built once, generically, and then applied. Nothing below asks instance search to recognise a carrier as a product.

def CategoryTheory.prodComp {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [AddCommGroup A₁] [AddCommGroup A₂] [AddCommGroup B₁] [AddCommGroup B₂] [AddCommGroup M₁] [AddCommGroup M₂] (c₁ : A₁ →+ B₁ →+ M₁) (c₂ : A₂ →+ B₂ →+ M₂) : A₁ × A₂ →+ B₁ × B₂ →+ M₁ × M₂

Componentwise biadditive composition on a pair of products.

Equations

• CategoryTheory.prodComp c₁ c₂ = AddMonoidHom.mk' (fun (a : A₁ × A₂) => ((c₁ a.1).comp (AddMonoidHom.fst B₁ B₂)).prod ((c₂ a.2).comp (AddMonoidHom.snd B₁ B₂))) ⋯

@[simp]

theorem CategoryTheory.prodComp_apply {A₁ : Type u_1} {A₂ : Type u_2} {B₁ : Type u_3} {B₂ : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [AddCommGroup A₁] [AddCommGroup A₂] [AddCommGroup B₁] [AddCommGroup B₂] [AddCommGroup M₁] [AddCommGroup M₂] (c₁ : A₁ →+ B₁ →+ M₁) (c₂ : A₂ →+ B₂ →+ M₂) (a : A₁ × A₂) (b : B₁ × B₂) : ((prodComp c₁ c₂) a) b = ((c₁ a.1) b.1, (c₂ a.2) b.2)

@[implicit_reducible]

instance CategoryTheory.DGCategory.prodStruct (C : Type u) (D : Type u') [DGCategory C] [DGCategory D] : DGCategoryStruct (C × D)

The product of two dg categories.

Equations

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

@[simp]

theorem CategoryTheory.DGCategory.prod_d_apply {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {X Y : C × D} (p q : ℤ) (f : ↑((DGCategoryStruct.dgHom X.1 Y.1).X p) × ↑((DGCategoryStruct.dgHom X.2 Y.2).X p)) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d p q)) f = ((AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X.1 Y.1).d p q)) f.1, (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X.2 Y.2).d p q)) f.2)

Prod.fst_add and friends do not fire on these goals: the operations carry the carrier's AddCommGroup instance, which is definitionally but not syntactically Prod's, and simp matches syntactically. These rfl lemmas say the same thing at the type the goals actually have.

The type matters twice over. Stating them at (prodComplex K L).X p is not enough — the goals are about (dgHom X Y).X p for the product instance, which is prodComplex … definitionally and not syntactically, so those versions miss as well. They have to be stated exactly here.

@[simp]

theorem CategoryTheory.DGCategory.dgProd_fst_add {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {X Y : C × D} {p : ℤ} (a b : ↑((DGCategoryStruct.dgHom X Y).X p)) : (a + b).1 = a.1 + b.1

@[simp]

theorem CategoryTheory.DGCategory.dgProd_snd_add {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {X Y : C × D} {p : ℤ} (a b : ↑((DGCategoryStruct.dgHom X Y).X p)) : (a + b).2 = a.2 + b.2

@[simp]

theorem CategoryTheory.DGCategory.dgProd_fst_units_smul {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {X Y : C × D} {p : ℤ} (c : ℤˣ) (a : ↑((DGCategoryStruct.dgHom X Y).X p)) : (c • a).1 = c • a.1

@[simp]

theorem CategoryTheory.DGCategory.dgProd_snd_units_smul {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {X Y : C × D} {p : ℤ} (c : ℤˣ) (a : ↑((DGCategoryStruct.dgHom X Y).X p)) : (c • a).2 = c • a.2

@[simp]

theorem CategoryTheory.DGCategory.prod_dgId {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (X : C × D) : DGCategoryStruct.dgId X = (DGCategoryStruct.dgId X.1, DGCategoryStruct.dgId X.2)

@[simp]

theorem CategoryTheory.DGCategory.prod_dgComp_apply {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {X Y Z : C × D} (p q r : ℤ) (h : p + q = r) (f : ↑((DGCategoryStruct.dgHom X.1 Y.1).X p) × ↑((DGCategoryStruct.dgHom X.2 Y.2).X p)) (g : ↑((DGCategoryStruct.dgHom Y.1 Z.1).X q) × ↑((DGCategoryStruct.dgHom Y.2 Z.2).X q)) : ((DGCategoryStruct.dgComp p q r h) f) g = (((DGCategoryStruct.dgComp p q r h) f.1) g.1, ((DGCategoryStruct.dgComp p q r h) f.2) g.2)

@[implicit_reducible]

instance CategoryTheory.DGCategory.prod {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] : DGCategory (C × D)

The product dg category. Every axiom holds componentwise and no sign enters, so each proof is Prod.ext followed by the corresponding axiom in each factor.

Equations

• CategoryTheory.DGCategory.prod = { toDGCategoryStruct := CategoryTheory.DGCategory.prodStruct C D, dgComp_assoc := ⋯, dgId_comp := ⋯, dgComp_id := ⋯, dgId_cocycle := ⋯, dgComp_leibniz := ⋯ }