Homogeneous maps of dg cones #
The degree-zero cone lift in Pretriangulated.Lift is sufficient for the
ordinary homotopy category, but not for constructing a dg functor objectwise
by cones. A dg functor must map every homogeneous morphism, not only closed
degree-zero ones.
For vertical maps a and b of degree p, a homogeneous square carries a
degree-p-1 homotopy with boundary
d k = (-1)^p (f₁ ≫ b - a ≫ f₂).
The induced cone map has degree p. Its source-component term is multiplied
by (-1)^p; this sign is forced by the diagrammatic Leibniz convention. With
it, differentiating the lift of a homogeneous square gives the strict lift of
d a and d b (homogeneousLift_d); the homotopy contributes exactly the
term that cancels the failure of the square to commute.
This file is the single owner of the cone lift. The degree-zero
IsConeOf.lift of Pretriangulated.Lift is homogeneousLift 0, and
HomotopySquare there is a HomogeneousSquare of degree zero whose vertical
maps are closed.
A homogeneous homotopy-commutative square between closed degree-zero arrows. No closedness is imposed on the vertical maps: their differentials are needed when the square is used as the value of a dg functor on an arbitrary homogeneous morphism.
- homotopy : ↑((DGCategoryStruct.dgHom X₁ Y₂).X (p - 1))
The chosen homotopy has degree one below the vertical maps.
- homotopy_boundary : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X₁ Y₂).d (p - 1) p)) self.homotopy = p.negOnePow • (((DGCategoryStruct.dgComp 0 p p ⋯) f₁) b - ((DGCategoryStruct.dgComp p 0 p ⋯) a) f₂)
The signed boundary equation.
Instances For
A strictly commuting homogeneous square, with zero homotopy.
Equations
- CategoryTheory.DGCategory.HomogeneousSquare.strict h = { homotopy := 0, homotopy_boundary := ⋯ }
Instances For
The homogeneous lift of a homotopy-commutative square to its chosen cone objects. The first term has the Koszul sign forced by differentiation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A homogeneous cone lift restricts to b on the target inclusion.
inr_comp_homogeneousLift with an arbitrary common result-degree name.
This form is convenient in graded naturality statements, whose composition
witnesses need not normalize their result index syntactically.
The shifted source inclusion is graded-natural for strict homogeneous
cone lifts. The factor (-1)^p is exactly the Koszul sign later required by
the degree--1 natural transformation from the source functor to its cone.
inl_comp_homogeneousLift_strict with an arbitrary common result-degree
name, for direct use in degree--1 graded naturality.
The homogeneous lift of the zero square is zero.
The strict homogeneous lift is additive in the vertical maps.
The source projection reads the signed source component of a homogeneous
cone lift. The homotopy term dies against inr ≫ fst = 0, so no strictness
is needed.
The target projection reads the target component of a strict homogeneous cone lift.
homogeneousLift_comp_fst with an arbitrary common result-degree name.
This is the form degree-one graded naturality asks for.
homogeneousLift_comp_snd with an arbitrary common result-degree name.
Two homogeneous maps into a cone are equal when their two cone projections agree. This is the all-degree analogue of extensionality for a binary direct sum, derived from the cone's splitting of the identity.
Strict homogeneous cone lifts preserve graded composition.
This theorem is the multiplicativity law required by the objectwise-cone dg functor. Its proof uses the two projection identities, so the sign is checked once at the canonical cone boundary rather than by re-expanding three cone formulas.
The homogeneous lift of a homotopy-commutative square commutes with the
differential. The differential of the degree-p lift is the strict
degree-p+1 lift of the differentials of its two vertical maps: the
a-term's differential is fst ≫ a ≫ f₂ ≫ inr, the b-term's is
-(fst ≫ f₁) ≫ b ≫ inr -- the cone's own correction -- and the boundary of
the homotopy is exactly their difference, so the three cancel and only the
d a and d b components survive.
This is the chain-map identity behind every cone functor in the repository;
the strict case homogeneousLift_strict_d and the degree-zero
IsConeOf.lift_closed are both instances of it.
The strict case of homogeneousLift_d: with a zero homotopy the square
commutes on the nose and the lift is a chain map.
The differential law for a strict homogeneous lift in arbitrary source
and target degrees. Off the cochain-complex successor diagonal all three
differentials vanish by shape; on the diagonal this is
homogeneousLift_strict_d.