Duality for curved duplexes #
Let X be a curved duplex of curvature w in FGModuleCat S whose two components are
projective modules, and let Xᵛ be its algebraic dual, with components X₀ᵛ and X₁ᵛ. The
duality used throughout the theory of matrix factorizations crosses the two differentials and
puts the single minus sign on the second one:
(Pᵛ)₀ = P₀ᵛ (Pᵛ)₁ = P₁ᵛ
d₀ᵛ = (d₁)ᵗ : P₀ᵛ ⟶ P₁ᵛ d₁ᵛ = -(d₀)ᵗ : P₁ᵛ ⟶ P₀ᵛ .
The two composites d₀ᵛ ≫ d₁ᵛ and d₁ᵛ ≫ d₀ᵛ are then both multiplication by -w, so duality
is a passage from curvature w to curvature -w. Transposition reverses composition, which is
why the differentials are crossed, and the sign is what compensates: a crossed pair of
transposes is the transpose of the original composite, and the minus sign turns w into -w.
Duality is contravariant, and this file records it as such: CurvedDuplex.dualMap sends a
morphism to a morphism from the dual of its target to the dual of its source, and reverses
identity and composition. Crossing the differentials twice therefore lands back at the original
curvature, with the negated double transposes as the differentials of a double dual, and the two
evaluations identify a double dual with the original duplex.
The two differential equations of the dual are the crossed-transpose computations
FGModuleCat.negDualMap_comp_dualMap and FGModuleCat.dualMap_negDualMap, the two placements of
the minus sign between the crossed transposes, and the two differential equations of the double
dual are its one-dual-further version FGModuleCat.negDualMap_dualMap_comp_negDualMap_dualMap.
Those three statements quantify over a curved pair of morphisms of FGModuleCat, so the curvature
is part of their hypothesis, and the only places they are used are the differential equations of
the duals defined below. They are proved here, in the FGModuleCat namespace their statements
belong to and beside those constructions, rather than in the module-duality file, which knows
nothing about curvature.
Main definitions #
CurvedDuplex.dual: the dual of a curved duplex with projective components, of curvature-w.CurvedDuplex.dualMap: the dual of a morphism of curved duplexes, contravariantly.CurvedDuplex.doubleDual,CurvedDuplex.doubleDualIso: the double dual, of the original curvature, and its isomorphism with the original duplex.
Main results #
CurvedDuplex.dual_d₀,CurvedDuplex.dual_d₁: the crossed transposed differentials.CurvedDuplex.dualMap_f₀,CurvedDuplex.dualMap_f₁: the components of a dual morphism are the transposes of the components;CurvedDuplex.dualMapitself is not exposed.CurvedDuplex.dualMap_id,CurvedDuplex.dualMap_comp,CurvedDuplex.dualMap_zero,CurvedDuplex.dualMap_add: the dual of a morphism reverses identity and composition and is additive, which is what makes duality contravariant.FGModuleCat.negDualMap_comp_dualMap,FGModuleCat.dualMap_negDualMap: the composite of the crossed transposes of a curved pair of morphisms, with the single minus sign on either of them, is multiplication by-won the dual. These are the two differential equations ofCurvedDuplex.dual.FGModuleCat.negDualMap_dualMap_comp_negDualMap_dualMap: the same computation one dual further, for the two negated double transposes, which is the original curvature again. This is what makes the two differential equations ofCurvedDuplex.doubleDualhold.CurvedDuplex.doubleDual_d₀,CurvedDuplex.doubleDual_d₁: the negated double transposes.CurvedDuplex.doubleDualIso,CurvedDuplex.doubleDualIso_f₀,CurvedDuplex.doubleDualIso_f₁: a double dual is isomorphic to the original curved duplex, by the evaluation pairing with the single minus sign on the even component.
Crossed-transpose curvature equations #
The three statements below are the differential equations of the duals defined in this file, and
they are proved here rather than in TauCeti.Algebra.Category.FGModuleCat.Dual: each of them
quantifies over a curved pair of morphisms, so the curvature is part of its hypothesis, and the
only places they are used are the d₀_comp_d₁ and d₁_comp_d₀ fields of the duals below. They
are stated in the FGModuleCat namespace, which is the namespace their statements belong to.
For a curved pair of maps f and g with f ≫ g = w • 𝟙, the composite of the negated
transpose of g with the transpose of f is multiplication by -w on the dual. This is one of
the two differential equations of a dual of curvature -w, the one in which the minus sign sits
on the left-hand factor of the composite; FGModuleCat.dualMap_negDualMap is the same
calculation with the minus sign on the right-hand factor.
The other placement of the minus sign: for a curved pair of maps f and g with
f ≫ g = w • 𝟙, the composite of the transpose of g with the negated transpose of f is
multiplication by -w on the dual. This is the other of the two differential equations of a
dual of curvature -w, the one in which the minus sign sits on the right-hand factor of the
composite. It is FGModuleCat.negDualMap_comp_dualMap read the other way round, since negating
either factor of a composite negates the composite.
The same computation one dual further: the composite of the two negated double transposes of
a curved pair of maps is multiplication by the original w on the double dual. This is the
computation behind the two differential equations of a double dual, and the reason a double dual
has the same curvature as its source.
The dual of a curved duplex with projective components is a curved duplex of the negated curvature whose differentials are the crossed transposes, the minus sign on the second.
Equations
- X.dual = { X₀ := FGModuleCat.dual S X.X₀, X₁ := FGModuleCat.dual S X.X₁, d₀ := FGModuleCat.dualMap X.d₁, d₁ := -FGModuleCat.dualMap X.d₀, d₀_comp_d₁ := ⋯, d₁_comp_d₀ := ⋯ }
Instances For
The even component of a dual curved duplex is the dual of the even component.
The odd component of a dual curved duplex is the dual of the odd component.
The even differential of a dual is the transpose of the odd differential of the original. The differentials are crossed because transposition reverses composition, so that the two composites of the dual are the transposes of the two composites of the original.
The odd differential of a dual is the negated transpose of the even differential of the
original. The single minus sign is what turns a curvature w into a curvature -w.
The dual of a morphism of curved duplexes is a morphism from the dual of the target to the
dual of the source, with transposed components. The two commutativity conditions of f enter
with the two differentials exchanged, which is what the crossed transposes need.
Equations
Instances For
The even component of the dual of a morphism of curved duplexes is the transpose of the even component of the morphism.
The odd component of the dual of a morphism of curved duplexes is the transpose of the odd component of the morphism.
Dualization is contravariant on morphisms: the dual of the identity of a curved duplex is the identity of its dual.
Dualization is contravariant on morphisms: the dual of a composite is the composite of the duals in the opposite order.
Dualization is contravariant on morphisms and additive: the dual of the zero morphism of a curved duplex is the zero morphism of its dual.
Dualization is contravariant on morphisms and additive: the dual of a sum of morphisms of curved duplexes is the sum of the duals.
The double dual of a curved duplex is a curved duplex of the same curvature: each of its
differentials is the negated double transpose of the corresponding differential of the original,
and the two minus signs cancel when the differentials are composed, so the composite is
multiplication by w again. The evaluation pairing with the single minus sign on the even
component identifies it with the original duplex, as CurvedDuplex.doubleDualIso records.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The even component of a double dual is the double dual of the even component.
The odd component of a double dual is the double dual of the odd component.
The even differential of a double dual is the negated double transpose of the even
differential of the original. Crossing twice no longer swaps the two components, and the two
minus signs cancel when the differentials are composed, so the curvature is w again.
The odd differential of a double dual is the negated double transpose of the odd differential of the original, with the sign on the odd component.
A double dual is isomorphic to the original curved duplex. The isomorphism is the evaluation pairing, with the single minus sign on the even component: that is the placement which makes the two commutativity conditions hold against the negated double transposes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The even component of the double dual isomorphism is the negated evaluation isomorphism.
The odd component of the double dual isomorphism is the evaluation isomorphism.
The even component of the inverse of the double dual isomorphism is the negated inverse evaluation isomorphism.
The odd component of the inverse of the double dual isomorphism is the inverse evaluation isomorphism.