Tensoring a dg object by a complex

The evaluation functor RHom(E,-) ⊗ E needs an object K ⊗ X for a complex K and an object X, and the repository has no tensor product to build it with: at the pinned Mathlib revision HomologicalComplex.HasTensor does not synthesize for the ℤ-indexed shape, which is the whole reason DGCategory encodes composition as a family of biadditive maps rather than a chain map out of a tensor product (ADR-0010, ADR-0011).

So the tensoring is stated the way IsShiftBy states the shift: by its universal property, as data plus a bijectivity condition, with no construction of the object. IsCopowerOf K X Z says Z is K ⊗ X, in the only sense that matters — degree-p morphisms out of Z are degree-p cochains out of K into the Hom-complex of X.

Why cochains are spelled out

A degree-p cochain K ⟶ dgHom X W is an additive map K i ⟶ (dgHom X W) j for every i + p = j. Mathlib's CochainComplex.HomComplex.Cochain packages exactly that, but naming it here would drag in the Triplet encoding and the δ API for no gain: the two conditions below are stated directly on the families, in the same vocabulary as the rest of this directory.

What the bijectivity is for

Everything. IsShiftBy gets its inverse, its uniqueness and its transport from one bijectivity assumption, and the same three follow here: IsCopowerOf.lift inverts the bijection, lift_unique says a morphism out of a copower is determined by the cochain it induces, and compare makes any two copowers of the same data canonically isomorphic in Z⁰.

HasCopower K X and HasCopowers C package mere existence in the same style as Mathlib's HasLimit and HasLimitsOfShape: the classes store no selected object, and the noncomputable copowerData API makes a choice only when a consumer asks for one. HasEvaluationData E is the narrower existence interface consumed by the object-twist construction; all copowers imply it.

The evaluation functor

EvaluationData E is a choice of copower of E by dgHom E X for every X, in the same shape as ConeData: objectwise data, assembled into a dg functor. Its functor is RHom(E,-) ⊗ E and its evaluation is the transformation to the identity, whose component at X is the morphism corresponding to the identity cochain of dgHom E X. Any two choices are connected by EvaluationData.compareIso, a canonical isomorphism in the closed degree-zero dg-functor category, and that comparison commutes strictly with evaluation.

Every one of the functor's four laws is lift_unique applied to the cochain each side induces; only map_d needs anything beyond associativity, and there it is the Leibniz rule twice, once in C and once in the Hom-complex.

What this does not give

Concrete existence. Nothing here proves that a particular dg category has copowers. Once a category supplies the HasCopowers capability, however, HasEvaluationData and chosenEvaluationData produce the evaluation data without adding compatibility fields or a second choice mechanism. Nothing here relates this functor to a spherical object: that comparison needs Perf(k) as a dg category, which the repository does not have.

def CategoryTheory.copowerCochain {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z : C} (univ : (i : ℤ) → ↑(K.X i) →+ ↑((DGCategoryStruct.dgHom X Z).X i)) {W : C} (p : ℤ) (g : ↑((DGCategoryStruct.dgHom Z W).X p)) (i j : ℤ) (h : i + p = j) : ↑(K.X i) →+ ↑((DGCategoryStruct.dgHom X W).X j)

The degree-p cochain that a degree-p morphism out of a copower induces: apply the universal family, then compose.

Equations

• CategoryTheory.copowerCochain univ p g i j h = AddMonoidHom.mk' (fun (x : ↑(K.X i)) => ((CategoryTheory.DGCategoryStruct.dgComp i p j h) ((univ i) x)) g) ⋯

@[simp]

theorem CategoryTheory.copowerCochain_apply {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z : C} (univ : (i : ℤ) → ↑(K.X i) →+ ↑((DGCategoryStruct.dgHom X Z).X i)) {W : C} (p : ℤ) (g : ↑((DGCategoryStruct.dgHom Z W).X p)) (i j : ℤ) (h : i + p = j) (x : ↑(K.X i)) : (copowerCochain univ p g i j h) x = ((DGCategoryStruct.dgComp i p j h) ((univ i) x)) g

structure CategoryTheory.IsCopowerOf {C : Type u} [DGCategory C] (K : CochainComplex AddCommGrpCat ℤ) (X Z : C) : Type v

Z is the tensoring of X by the complex K.

The data is a chain map K ⟶ dgHom X Z, and the condition is that composing with it identifies degree-p morphisms out of Z with degree-p cochains out of K, for every degree and every target. This is IsShiftBy's pattern: the object is not built, only characterised.

• univ (i : ℤ) : ↑(K.X i) →+ ↑((DGCategoryStruct.dgHom X Z).X i)

  The universal family, degree by degree.

• univ_d (i j : ℤ) (x : ↑(K.X i)) : (self.univ j) ((AddCommGrpCat.Hom.hom (K.d i j)) x) = (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Z).d i j)) ((self.univ i) x)

  It is a chain map.

• bijective (W : C) (p : ℤ) : Function.Bijective fun (g : ↑((DGCategoryStruct.dgHom Z W).X p)) => copowerCochain self.univ p g

  Composing with it is bijective onto cochains, in every degree and from every target.

theorem CategoryTheory.IsCopowerOf.lift_unique {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z : C} (t : IsCopowerOf K X Z) {W : C} {p : ℤ} {g g' : ↑((DGCategoryStruct.dgHom Z W).X p)} (h : ∀ (i j : ℤ) (hij : i + p = j) (x : ↑(K.X i)), ((DGCategoryStruct.dgComp i p j hij) ((t.univ i) x)) g = ((DGCategoryStruct.dgComp i p j hij) ((t.univ i) x)) g') : g = g'

A morphism out of a copower is determined by the cochain it induces.

noncomputable def CategoryTheory.IsCopowerOf.lift {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z : C} (t : IsCopowerOf K X Z) {W : C} (p : ℤ) (c : (i j : ℤ) → i + p = j → ↑(K.X i) →+ ↑((DGCategoryStruct.dgHom X W).X j)) : ↑((DGCategoryStruct.dgHom Z W).X p)

Every cochain out of K is induced by a morphism out of the copower.

Equations

• t.lift p c = ⋯.choose

@[simp]

theorem CategoryTheory.IsCopowerOf.univ_comp_lift {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z : C} (t : IsCopowerOf K X Z) {W : C} (p : ℤ) (c : (i j : ℤ) → i + p = j → ↑(K.X i) →+ ↑((DGCategoryStruct.dgHom X W).X j)) (i j : ℤ) (hij : i + p = j) (x : ↑(K.X i)) : ((DGCategoryStruct.dgComp i p j hij) ((t.univ i) x)) (t.lift p c) = (c i j hij) x

noncomputable def CategoryTheory.IsCopowerOf.compare {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z Z' : C} (t : IsCopowerOf K X Z) (t' : IsCopowerOf K X Z') : ↑((DGCategoryStruct.dgHom Z Z').X 0)

The comparison between two copowers of the same data: the lift of the other one's universal family.

The index is normalised with cases rather than subst: the cochain is indexed by i + 0 = j, and j is the variable that has to go.

Equations

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

@[simp]

theorem CategoryTheory.IsCopowerOf.univ_comp_compare {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z Z' : C} (t : IsCopowerOf K X Z) (t' : IsCopowerOf K X Z') (i : ℤ) (x : ↑(K.X i)) : ((DGCategoryStruct.dgComp i 0 i ⋯) ((t.univ i) x)) (t.compare t') = (t'.univ i) x

theorem CategoryTheory.IsCopowerOf.compare_mem_cocycles {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z Z' : C} (t : IsCopowerOf K X Z) (t' : IsCopowerOf K X Z') : t.compare t' ∈ cocycles Z Z'

The canonical comparison is closed, hence is a morphism in Z⁰ C.

Both universal families are chain maps. Applying the Leibniz rule to the source universal family followed by the comparison leaves the differential of the comparison as the only unmatched term, and the universal property detects that it vanishes.

theorem CategoryTheory.IsCopowerOf.compare_comp_compare {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z Z' : C} (t : IsCopowerOf K X Z) (t' : IsCopowerOf K X Z') : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (t.compare t')) (t'.compare t) = DGCategoryStruct.dgId Z

Any two copowers of the same data are canonically isomorphic. The two comparisons compose to the identity, so the object IsCopowerOf characterises is unique up to a canonical degree-zero isomorphism.

theorem CategoryTheory.IsCopowerOf.compare_trans {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z Z' Z'' : C} (t : IsCopowerOf K X Z) (t' : IsCopowerOf K X Z') (t'' : IsCopowerOf K X Z'') : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (t.compare t')) (t'.compare t'') = t.compare t''

Canonical copower comparisons compose. Together with compare_comp_compare and compare_self, this makes the copower choices for fixed K and X a contractible groupoid inside Z⁰ C.

@[simp]

theorem CategoryTheory.IsCopowerOf.compare_self {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z : C} (t : IsCopowerOf K X Z) : t.compare t = DGCategoryStruct.dgId Z

Comparing a copower with itself is the identity.

structure CategoryTheory.CopowerData {C : Type u} [DGCategory C] (K : CochainComplex AddCommGrpCat ℤ) (X : C) : Type (max u v)

A copower object together with its universal-property witness.

• obj : C

  The chosen copower object.

• isCopower : IsCopowerOf K X self.obj

  The universal property witnessed by the chosen object.

class CategoryTheory.HasCopower {C : Type u} [DGCategory C] (K : CochainComplex AddCommGrpCat ℤ) (X : C) : Prop

Mere existence of a copower of X by K.

Like Mathlib's HasLimit, this proposition carries no preferred choice in its public contract. The choice is made only by copowerData.

• exists_copower : Nonempty (CopowerData K X)

theorem CategoryTheory.HasCopower.of_isCopower {C : Type u} [DGCategory C] {K : CochainComplex AddCommGrpCat ℤ} {X Z : C} (t : IsCopowerOf K X Z) : HasCopower K X

A witnessed copower supplies the corresponding existence instance.

noncomputable def CategoryTheory.copowerData {C : Type u} [DGCategory C] (K : CochainComplex AddCommGrpCat ℤ) (X : C) [HasCopower K X] : CopowerData K X

A noncomputably selected copower and its witness.

Equations

• CategoryTheory.copowerData K X = Classical.choice ⋯

noncomputable def CategoryTheory.copowerObj {C : Type u} [DGCategory C] (K : CochainComplex AddCommGrpCat ℤ) (X : C) [HasCopower K X] : C

The copower object selected from HasCopower K X.

Equations

• CategoryTheory.copowerObj K X = (CategoryTheory.copowerData K X).obj

noncomputable def CategoryTheory.copowerIsCopower {C : Type u} [DGCategory C] (K : CochainComplex AddCommGrpCat ℤ) (X : C) [HasCopower K X] : IsCopowerOf K X (copowerObj K X)

The universal-property witness for the selected copowerObj K X.

Equations

• CategoryTheory.copowerIsCopower K X = (CategoryTheory.copowerData K X).isCopower

class CategoryTheory.HasCopowers (C : Type u) [DGCategory C] : Prop

Existence of all copowers by integer cochain complexes.

• has_copower (K : CochainComplex AddCommGrpCat ℤ) (X : C) : HasCopower K X

@[instance 100]

instance CategoryTheory.hasCopowerOfHasCopowers {C : Type u} [DGCategory C] [HasCopowers C] (K : CochainComplex AddCommGrpCat ℤ) (X : C) : HasCopower K X

All copowers give each individual copower. The low priority leaves room for a category to expose a more specific local construction.

structure CategoryTheory.EvaluationData {C : Type u} [DGCategory C] (E : C) : Type (max u v)

A choice of RHom(E,X) ⊗ E for every X.

The same shape as HomogeneousNatTrans.ConeData: objectwise data that the next declarations assemble into a dg functor.

• obj : C → C

  The chosen object RHom(E,X) ⊗ E.

• isCopower (X : C) : IsCopowerOf (DGCategoryStruct.dgHom E X) E (self.obj X)

  It is the copower of E by the Hom-complex out of E.

class CategoryTheory.HasEvaluationData {C : Type u} [DGCategory C] (E : C) : Prop

Mere existence of the copowers needed for evaluation at E.

• exists_evaluationData : Nonempty (EvaluationData E)

noncomputable def CategoryTheory.chosenEvaluationData {C : Type u} [DGCategory C] (E : C) [HasEvaluationData E] : EvaluationData E

Evaluation data noncomputably selected from HasEvaluationData E.

Equations

• CategoryTheory.chosenEvaluationData E = Classical.choice ⋯

noncomputable def CategoryTheory.EvaluationData.ofHasCopowers {C : Type u} [DGCategory C] [HasCopowers C] (E : C) : EvaluationData E

All copowers supply the family of copowers needed for evaluation at E.

Equations

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

@[instance 100]

instance CategoryTheory.EvaluationData.hasEvaluationDataOfHasCopowers {C : Type u} [DGCategory C] [HasCopowers C] (E : C) : HasEvaluationData E

A category with all copowers has evaluation data at every object.

noncomputable def CategoryTheory.EvaluationData.map {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ↑((DGCategoryStruct.dgHom (V.obj X) (V.obj Y)).X p)

The action on a homogeneous morphism: postcompose inside the Hom-complex, then lift.

Equations

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

@[simp]

theorem CategoryTheory.EvaluationData.univ_comp_map {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (i j : ℤ) (hij : i + p = j) (k : ↑((DGCategoryStruct.dgHom E X).X i)) : ((DGCategoryStruct.dgComp i p j hij) (((V.isCopower X).univ i) k)) (V.map p f) = ((V.isCopower Y).univ j) (((DGCategoryStruct.dgComp i p j hij) k) f)

@[simp]

theorem CategoryTheory.EvaluationData.map_zero {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) {X Y : C} (p : ℤ) : V.map p 0 = 0

theorem CategoryTheory.EvaluationData.map_add {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) {X Y : C} (p : ℤ) (f f' : ↑((DGCategoryStruct.dgHom X Y).X p)) : V.map p (f + f') = V.map p f + V.map p f'

noncomputable def CategoryTheory.EvaluationData.functor {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) : DGFunctor C C

The evaluation functor RHom(E,-) ⊗ E.

Equations

• V.functor = { obj := V.obj, map := fun {X Y : C} (p : ℤ) => AddMonoidHom.mk' (V.map p) ⋯, map_d := ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.EvaluationData.functor_obj {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) (X : C) : V.functor.obj X = V.obj X

theorem CategoryTheory.EvaluationData.functor_map {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (V.functor.map p) f = V.map p f

Not @[simp]: functor_obj rewrites inside this statement's own type, so the left-hand side is not in simp normal form and simpNF rejects it. The same reason keeps DGFunctor.shiftedFunctor_map off the simp set.

noncomputable def CategoryTheory.EvaluationData.evalHom {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) (X : C) : ↑((DGCategoryStruct.dgHom (V.obj X) X).X 0)

The evaluation morphism at X: the morphism RHom(E,X) ⊗ E ⟶ X induced by the identity cochain of dgHom E X. That is exactly what "evaluate" means.

The index is normalised with cases rather than subst, for the reason given at IsCopowerOf.compare.

Equations

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

@[simp]

theorem CategoryTheory.EvaluationData.univ_comp_evalHom {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) (X : C) (i : ℤ) (k : ↑((DGCategoryStruct.dgHom E X).X i)) : ((DGCategoryStruct.dgComp i 0 i ⋯) (((V.isCopower X).univ i) k)) (V.evalHom X) = k

noncomputable def CategoryTheory.EvaluationData.evaluation {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) : ↥(V.functor.HomogeneousNatTrans (DGFunctor.id C) 0)

The evaluation transformation RHom(E,-) ⊗ E ⟶ id.

It is homogeneous of degree zero, so its Koszul sign is trivial and naturality is the plain square: both sides are the cochain k ↦ k · f.

Equations

• V.evaluation = ⟨V.evalHom, ⋯⟩

theorem CategoryTheory.EvaluationData.evaluation_isClosed {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) : DGFunctor.HomogeneousNatTrans.IsClosed V.evaluation

The evaluation transformation is closed.

Componentwise this is the Leibniz rule against the identity cochain: the universal family is a chain map, so differentiating univ i k · eval produces the same term twice, once from each factor, and the factor that carries d eval is what is left.

Closedness is what lets evaluation have a cone, which is the twist.

noncomputable def CategoryTheory.EvaluationData.compare {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) : ↥(V.functor.HomogeneousNatTrans W.functor 0)

The canonical closed natural comparison between two choices of evaluation data. Objectwise it is the canonical comparison between their copowers.

Equations

• V.compare W = ⟨fun (Y : C) => (V.isCopower Y).compare (W.isCopower Y), ⋯⟩

@[simp]

theorem CategoryTheory.EvaluationData.compare_app {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) (Y : C) : DGFunctor.HomogeneousNatTrans.app (V.compare W) Y = (V.isCopower Y).compare (W.isCopower Y)

theorem CategoryTheory.EvaluationData.compare_isClosed {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) : DGFunctor.HomogeneousNatTrans.IsClosed (V.compare W)

The canonical comparison is closed because its components are closed.

theorem CategoryTheory.EvaluationData.compare_comp {C : Type u} [DGCategory C] {E : C} (V W U : EvaluationData E) : ((DGFunctor.HomogeneousNatTrans.composition V.functor W.functor U.functor 0 0 0 ⋯) (V.compare W)) (W.compare U) = V.compare U

Canonical comparisons compose strictly.

@[simp]

theorem CategoryTheory.EvaluationData.compare_self {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) : V.compare V = DGFunctor.HomogeneousNatTrans.id V.functor

The comparison from an evaluation choice to itself is the identity.

noncomputable def CategoryTheory.EvaluationData.compareIso {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) : (have this := V.functor; this) ≅ have this := W.functor; this

The canonical comparison between two evaluation choices as an isomorphism in the closed degree-zero dg-functor category.

Equations

• V.compareIso W = { hom := ⟨V.compare W, ⋯⟩, inv := ⟨W.compare V, ⋯⟩, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.EvaluationData.compareIso_hom_val {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) : ↑(V.compareIso W).hom = V.compare W

@[simp]

theorem CategoryTheory.EvaluationData.compareIso_inv_val {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) : ↑(V.compareIso W).inv = W.compare V

@[simp]

theorem CategoryTheory.EvaluationData.compareIso_self {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) : V.compareIso V = Iso.refl (have this := V.functor; this)

The canonical evaluation-data comparison from a choice to itself is the identity isomorphism.

theorem CategoryTheory.EvaluationData.compareIso_trans {C : Type u} [DGCategory C] {E : C} (V W U : EvaluationData E) : V.compareIso W ≪≫ W.compareIso U = V.compareIso U

Canonical evaluation-data comparison isomorphisms are transitive.

theorem CategoryTheory.EvaluationData.compare_comp_evaluation {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) : ((DGFunctor.HomogeneousNatTrans.composition V.functor W.functor (DGFunctor.id C) 0 0 0 ⋯) (V.compare W)) W.evaluation = V.evaluation

The canonical comparison commutes strictly with evaluation.