Homogeneous natural transformations of dg functors

For dg functors F G : C ⟶ D, a homogeneous natural transformation of degree n has components F X ⟶ G X of degree n and satisfies graded naturality

F f ≫ η Y = (-1)^(n * p) • (η X ≫ G f)

for every homogeneous f : X ⟶ Y of degree p. The sign convention is written for this repository's diagrammatic dgComp.

The natural transformations of every degree form an additive subgroup of the product of the component Hom-groups. Packaging them that way gives the additive structure by restriction rather than re-proving the group laws for a large record. The pointwise differential and vertical composition defined below are the ingredients of the dg category of dg functors.

@[reducible, inline]

abbrev CategoryTheory.DGFunctor.HomogeneousFamily {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F G : DGFunctor C D) (n : ℤ) : Type (max u v)

Families of degree-n components between two dg functors.

Equations

• F.HomogeneousFamily G n = ((X : C) → ↑((CategoryTheory.DGCategoryStruct.dgHom (F.obj X) (G.obj X)).X n))

def CategoryTheory.DGFunctor.HomogeneousFamily.IsNatural {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : F.HomogeneousFamily G n) : Prop

Graded naturality for a family of degree-n components.

The common result degree is quantified explicitly. This mirrors the repository's dgComp p q r h encoding and lets later Leibniz arguments choose one fibre for all terms instead of inserting transports between associatively or commutatively equal integer expressions.

Equations

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

def CategoryTheory.DGFunctor.homogeneousNatTransSubgroup {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F G : DGFunctor C D) (n : ℤ) : AddSubgroup (F.HomogeneousFamily G n)

The additive subgroup of component families satisfying graded naturality.

Equations

• F.homogeneousNatTransSubgroup G n = { carrier := CategoryTheory.DGFunctor.HomogeneousFamily.IsNatural, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.DGFunctor.HomogeneousNatTrans {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F G : DGFunctor C D) (n : ℤ) : AddSubgroup (F.HomogeneousFamily G n)

A homogeneous dg natural transformation, as the natural-family subgroup.

Equations

• F.HomogeneousNatTrans G n = F.homogeneousNatTransSubgroup G n

def CategoryTheory.DGFunctor.HomogeneousNatTrans.app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (X : C) : ↑((DGCategoryStruct.dgHom (F.obj X) (G.obj X)).X n)

The component of a homogeneous dg natural transformation.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.app η X = ↑η X

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.zero_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (X : C) : app 0 X = 0

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.add_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η θ : ↥(F.HomogeneousNatTrans G n)) (X : C) : app (η + θ) X = app η X + app θ X

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.neg_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (X : C) : app (-η) X = -app η X

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.zsmul_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (a : ℤ) (η : ↥(F.HomogeneousNatTrans G n)) (X : C) : app (a • η) X = a • app η X

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.units_smul_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (a : ℤˣ) (η : ↥(F.HomogeneousNatTrans G n)) (X : C) : app (a • η) X = a • app η X

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.naturality {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) {X Y : C} (p r : ℤ) (hpn : p + n = r) (hnp : n + p = r) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((DGCategoryStruct.dgComp p n r hpn) ((F.map p) f)) (app η Y) = (n * p).negOnePow • ((DGCategoryStruct.dgComp n p r hnp) (app η X)) ((G.map p) f)

Graded naturality, exposed from subgroup membership.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ext {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} {η θ : ↥(F.HomogeneousNatTrans G n)} (h : ∀ (X : C), app η X = app θ X) : η = θ

Homogeneous transformations are equal when all components are equal.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ext_iff {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} {η θ : ↥(F.HomogeneousNatTrans G n)} : η = θ ↔ ∀ (X : C), app η X = app θ X

def CategoryTheory.DGFunctor.HomogeneousNatTrans.id {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : ↥(F.HomogeneousNatTrans F 0)

The degree-zero identity dg natural transformation.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.id F = ⟨fun (X : C) => CategoryTheory.DGCategoryStruct.dgId (F.obj X), ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.id_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X : C) : app (id F) X = DGCategoryStruct.dgId (F.obj X)

def CategoryTheory.DGFunctor.HomogeneousNatTrans.comp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G H : DGFunctor C D} {n m : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (θ : ↥(G.HomogeneousNatTrans H m)) : ↥(F.HomogeneousNatTrans H (n + m))

Vertical composition of homogeneous dg natural transformations.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.comp_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G H : DGFunctor C D} {n m : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (θ : ↥(G.HomogeneousNatTrans H m)) (X : C) : app (comp η θ) X = ((DGCategoryStruct.dgComp n m (n + m) ⋯) (app η X)) (app θ X)

def CategoryTheory.DGFunctor.HomogeneousNatTrans.differential {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) : ↥(F.HomogeneousNatTrans G (n + 1))

The pointwise differential of a homogeneous dg natural transformation.

Its graded naturality is not merely pointwise: the proof differentiates the naturality equation for η, then uses naturality of η once more on d f. The two extra terms cancel after the Koszul signs are normalized.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.differential_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (X : C) : app (differential η) X = (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom (F.obj X) (G.obj X)).d n (n + 1))) (app η X)

def CategoryTheory.DGFunctor.HomogeneousNatTrans.IsClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) : Prop

A homogeneous dg natural transformation is closed when its pointwise differential vanishes. Keeping this predicate at the dg-functor root lets cones, adjunctions, and future enriched constructions share one notion.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.IsClosed η = (CategoryTheory.DGFunctor.HomogeneousNatTrans.differential η = 0)

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.IsClosed.app_d {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} {η : ↥(F.HomogeneousNatTrans G n)} (hη : IsClosed η) (X : C) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom (F.obj X) (G.obj X)).d n (n + 1))) (app η X) = 0

Every component of a closed homogeneous dg natural transformation is closed in the corresponding Hom-complex.

def CategoryTheory.DGFunctor.HomogeneousNatTrans.differentialHom {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F G : DGFunctor C D) (n : ℤ) : ↥(F.HomogeneousNatTrans G n) →+ ↥(F.HomogeneousNatTrans G (n + 1))

The pointwise differential as an additive homomorphism.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.differentialHom F G n = { toFun := CategoryTheory.DGFunctor.HomogeneousNatTrans.differential, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.differentialHom_apply {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) : (differentialHom F G n) η = differential η

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.differential_differential {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) : differential (differential η) = 0

The pointwise differential squares to zero.

@[reducible]

def CategoryTheory.DGFunctor.HomogeneousNatTrans.complex {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F G : DGFunctor C D) : CochainComplex AddCommGrpCat ℤ

The Hom-complex of homogeneous dg natural transformations.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.complex_X {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F G : DGFunctor C D) (n : ℤ) : (complex F G).X n = AddCommGrpCat.of ↥(F.HomogeneousNatTrans G n)

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.complex_d_apply {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {n : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) : (AddCommGrpCat.Hom.hom ((complex F G).d n (n + 1))) η = differential η

@[reducible]

def CategoryTheory.DGFunctor.HomogeneousNatTrans.composition {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F G H : DGFunctor C D) (n m r : ℤ) (h : n + m = r) : ↥(F.HomogeneousNatTrans G n) →+ ↥(G.HomogeneousNatTrans H m) →+ ↥(F.HomogeneousNatTrans H r)

Biadditive vertical composition in an arbitrary result degree.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.composition_apply_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G H : DGFunctor C D} {n m : ℤ} (η : ↥(F.HomogeneousNatTrans G n)) (θ : ↥(G.HomogeneousNatTrans H m)) (r : ℤ) (h : n + m = r) (X : C) : app (((composition F G H n m r h) η) θ) X = ((DGCategoryStruct.dgComp n m r h) (app η X)) (app θ X)

@[implicit_reducible]

noncomputable instance CategoryTheory.DGFunctor.dgCategory {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] : DGCategory (DGFunctor C D)

Dg functors C ⟶ D, homogeneous dg natural transformations, and their pointwise differential form a dg category.

Equations

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