Scalar-linear evaluation data in a dg category

LinearEvaluationData k E chooses the k-linear copower DGLinear.homComplex k E X ⊗ E for every object X. The universal properties assemble into a k-linear dg functor, and lifting the identity cochain gives a closed evaluation transformation to the identity functor.

The action cochain is built from DGLinear.postcompCochain: postcomposition by f : X ⟶ Y first sends Hom(E,X) to Hom(E,Y), then the universal chain map for the target sends it to Hom(E, Hom(E,Y) ⊗ E). Thus the construction uses Mathlib's HomComplex.Cochain composition rather than another componentwise cochain interface.

This is deliberately parallel to, not a refinement of, additive EvaluationData. Its copowers represent only k-linear cochains, so there is no general map from LinearEvaluationData to EvaluationData. Coefficient- complex homotopy invariance is supplied separately by LinearCopowerFunctor; this file stops before cones, exactness, Euler-class formulas, finite presentations, or concrete existence.

structure CategoryTheory.LinearEvaluationData (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (E : C) : Type (max u v)

A choice of the scalar-linear copower Hom(E,X) ⊗ E for every X.

• obj : C → C

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

• isLinearCopower (X : C) : IsLinearCopowerOf k (DGLinear.homComplex k E X) E (self.obj X)

  The chosen object has the scalar-linear copower universal property.

class CategoryTheory.HasLinearEvaluationData (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (E : C) : Prop

Mere existence of scalar-linear evaluation data at E.

• exists_linearEvaluationData : Nonempty (LinearEvaluationData k E)

noncomputable def CategoryTheory.chosenLinearEvaluationData (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (E : C) [HasLinearEvaluationData k E] : LinearEvaluationData k E

Scalar-linear evaluation data selected from its existence capability.

Equations

• CategoryTheory.chosenLinearEvaluationData k E = Classical.choice ⋯

noncomputable def CategoryTheory.LinearEvaluationData.ofHasLinearCopowers (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] (E : C) : LinearEvaluationData k E

All scalar-linear copowers supply scalar-linear evaluation data at E.

Equations

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

@[instance 100]

instance CategoryTheory.LinearEvaluationData.hasLinearEvaluationDataOfHasLinearCopowers (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] (E : C) : HasLinearEvaluationData k E

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

noncomputable def CategoryTheory.LinearEvaluationData.map {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) {X Y : C} (p : ℤ) : ↑((DGCategoryStruct.dgHom X Y).X p) →ₗ[k] ↑((DGCategoryStruct.dgHom (V.obj X) (V.obj Y)).X p)

The scalar-linear action on homogeneous morphisms.

Equations

• V.map p = ↑((V.isLinearCopower X).cochainLinearEquiv (V.obj Y) p).symm ∘ₗ CategoryTheory.LinearEvaluationData.mapCochain✝ V p

@[simp]

theorem CategoryTheory.LinearEvaluationData.univ_comp_map {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (i j : ℤ) (hij : i + p = j) (g : ↑((DGCategoryStruct.dgHom E X).X i)) : ((DGCategoryStruct.dgComp i p j hij) ((ConcreteCategory.hom ((V.isLinearCopower X).univ.f i)) g)) ((V.map p) f) = (ConcreteCategory.hom ((V.isLinearCopower Y).univ.f j)) (((DGCategoryStruct.dgComp i p j hij) g) f)

noncomputable def CategoryTheory.LinearEvaluationData.functor {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) : DGFunctor C C

The scalar-linear evaluation functor Hom(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.LinearEvaluationData.functor_obj {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) (X : C) : V.functor.obj X = V.obj X

theorem CategoryTheory.LinearEvaluationData.functor_map {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (V.functor.map p) f = (V.map p) f

Kept out of the simp set for the same normal-form reason as the additive evaluation functor's map projection.

instance CategoryTheory.LinearEvaluationData.functorLinear {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) : DGFunctor.Linear k V.functor

The scalar-linear evaluation functor preserves the k-action.

noncomputable def CategoryTheory.LinearEvaluationData.evalHom {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) (X : C) : ↑((DGCategoryStruct.dgHom (V.obj X) X).X 0)

The evaluation morphism corresponding to the identity cochain of DGLinear.homComplex k E X.

Equations

• V.evalHom X = (V.isLinearCopower X).lift 0 (CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id (CategoryTheory.DGLinear.homComplex k E X)))

@[simp]

theorem CategoryTheory.LinearEvaluationData.univ_comp_evalHom {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) (X : C) (i : ℤ) (g : ↑((DGCategoryStruct.dgHom E X).X i)) : ((DGCategoryStruct.dgComp i 0 i ⋯) ((ConcreteCategory.hom ((V.isLinearCopower X).univ.f i)) g)) (V.evalHom X) = g

noncomputable def CategoryTheory.LinearEvaluationData.evaluation {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) : ↥(V.functor.HomogeneousNatTrans (DGFunctor.id C) 0)

The closed degree-zero evaluation transformation Hom(E,-) ⊗ E ⟶ id.

Equations

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

theorem CategoryTheory.LinearEvaluationData.evaluation_isClosed {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) : DGFunctor.HomogeneousNatTrans.IsClosed V.evaluation

The scalar-linear evaluation transformation is closed.

noncomputable def CategoryTheory.LinearEvaluationData.compare {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W : LinearEvaluationData k E) : ↥(V.functor.HomogeneousNatTrans W.functor 0)

The canonical closed natural comparison between two scalar-linear evaluation choices.

Equations

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

@[simp]

theorem CategoryTheory.LinearEvaluationData.compare_app {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W : LinearEvaluationData k E) (Y : C) : DGFunctor.HomogeneousNatTrans.app (V.compare W) Y = (V.isLinearCopower Y).compare (W.isLinearCopower Y)

theorem CategoryTheory.LinearEvaluationData.compare_isClosed {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W : LinearEvaluationData k E) : DGFunctor.HomogeneousNatTrans.IsClosed (V.compare W)

The canonical scalar-linear evaluation comparison is closed.

theorem CategoryTheory.LinearEvaluationData.compare_comp {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W U : LinearEvaluationData k E) : ((DGFunctor.HomogeneousNatTrans.composition V.functor W.functor U.functor 0 0 0 ⋯) (V.compare W)) (W.compare U) = V.compare U

Canonical scalar-linear evaluation comparisons compose strictly.

@[simp]

theorem CategoryTheory.LinearEvaluationData.compare_self {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) : V.compare V = DGFunctor.HomogeneousNatTrans.id V.functor

The scalar-linear evaluation comparison from a choice to itself is the identity.

noncomputable def CategoryTheory.LinearEvaluationData.compareIso {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W : LinearEvaluationData k E) : (have this := V.functor; this) ≅ have this := W.functor; this

The canonical comparison 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.LinearEvaluationData.compareIso_hom_val {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W : LinearEvaluationData k E) : ↑(V.compareIso W).hom = V.compare W

@[simp]

theorem CategoryTheory.LinearEvaluationData.compareIso_inv_val {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W : LinearEvaluationData k E) : ↑(V.compareIso W).inv = W.compare V

@[simp]

theorem CategoryTheory.LinearEvaluationData.compareIso_self {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V : LinearEvaluationData k E) : V.compareIso V = Iso.refl (have this := V.functor; this)

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

theorem CategoryTheory.LinearEvaluationData.compareIso_trans {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W U : LinearEvaluationData k E) : V.compareIso W ≪≫ W.compareIso U = V.compareIso U

Canonical scalar-linear evaluation comparison isomorphisms are transitive.

theorem CategoryTheory.LinearEvaluationData.compare_comp_evaluation {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {E : C} (V W : LinearEvaluationData k 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 scalar-linear evaluation.