Relations between extend
and restriction
#
Given an embedding e : Embedding c c'
of complex shapes satisfying e.IsRelIff
,
we obtain a bijection e.homEquiv
between the type of morphisms
K ⟶ L.extend e
(with K : HomologicalComplex C c'
and L : HomologicalComplex C c
)
and the subtype of morphisms φ : K.restriction e ⟶ L
which satisfy a certain
condition e.HasLift φ
.
TODO #
- obtain dual results for morphisms
L.extend e ⟶ K
.
The condition on a morphism K.restriction e ⟶ L
which allows to
extend it as a morphism K ⟶ L.extend e
, see Embedding.homEquiv
.
Equations
Instances For
Auxiliary definition for liftExtend
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The morphism K ⟶ L.extend e
given by a morphism K.restriction e ⟶ L
which satisfy e.HasLift φ
.
Equations
- e.liftExtend φ hφ = { f := fun (i' : ι') => ComplexShape.Embedding.liftExtend.f φ i', comm' := ⋯ }
Instances For
Given φ : K.restriction e ⟶ L
such that hφ : e.HasLift φ
, this is
the isomorphisms in the category of arrows between the maps
(e.liftExtend φ hφ).f i'
and φ.f i
when e.f i = i'
.
Equations
Instances For
Auxiliary definition for Embedding.homRestrict
.
Equations
Instances For
The morphism K.restriction e ⟶ L
induced by a morphism K ⟶ L.extend e
.
Equations
- e.homRestrict ψ = { f := fun (i : ι) => ComplexShape.Embedding.homRestrict.f ψ i, comm' := ⋯ }
Instances For
The bijection between K ⟶ L.extend e
and the subtype of K.restriction e ⟶ L
consisting of morphisms φ
such that e.HasLift φ
.
Equations
- One or more equations did not get rendered due to their size.