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.
def
ComplexShape.Embedding.HasLift
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
:
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
noncomputable def
ComplexShape.Embedding.liftExtend.f
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(i' : ι')
:
Auxiliary definition for liftExtend.
Equations
Instances For
theorem
ComplexShape.Embedding.liftExtend.f_eq
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
{i' : ι'}
{i : ι}
(hi : e.f i = i')
:
f φ i' = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).inv
(CategoryTheory.CategoryStruct.comp (φ.f i) (L.extendXIso e hi).inv)
@[simp]
theorem
ComplexShape.Embedding.liftExtend.comm
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
(i' j' : ι')
:
CategoryTheory.CategoryStruct.comp (f φ i') ((L.extend e).d i' j') = CategoryTheory.CategoryStruct.comp (K.d i' j') (f φ j')
@[simp]
theorem
ComplexShape.Embedding.liftExtend.comm_assoc
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
(i' j' : ι')
{Z : C}
(h : (L.extend e).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (f φ i') (CategoryTheory.CategoryStruct.comp ((L.extend e).d i' j') h) = CategoryTheory.CategoryStruct.comp (K.d i' j') (CategoryTheory.CategoryStruct.comp (f φ j') h)
noncomputable def
ComplexShape.Embedding.liftExtend
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
:
The morphism K ⟶ L.extend e given by a morphism K.restriction e ⟶ L
which satisfy e.HasLift φ.
Equations
Instances For
theorem
ComplexShape.Embedding.liftExtend_f
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
{i' : ι'}
{i : ι}
(hi : e.f i = i')
:
(e.liftExtend φ hφ).f i' = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hi).inv
(CategoryTheory.CategoryStruct.comp (φ.f i) (L.extendXIso e hi).inv)
noncomputable def
ComplexShape.Embedding.liftExtendfArrowIso
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
{i' : ι'}
{i : ι}
(hi : e.f i = i')
:
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
theorem
ComplexShape.Embedding.isIso_liftExtend_f_iff
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
{i' : ι'}
{i : ι}
(hi : e.f i = i')
:
theorem
ComplexShape.Embedding.mono_liftExtend_f_iff
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
{i' : ι'}
{i : ι}
(hi : e.f i = i')
:
theorem
ComplexShape.Embedding.epi_liftExtend_f_iff
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
{i' : ι'}
{i : ι}
(hi : e.f i = i')
:
noncomputable def
ComplexShape.Embedding.homRestrict.f
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
(i : ι)
:
Auxiliary definition for Embedding.homRestrict.
Equations
Instances For
theorem
ComplexShape.Embedding.homRestrict.f_eq
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
{i : ι}
{i' : ι'}
(h : e.f i = i')
:
f ψ i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e h).hom
(CategoryTheory.CategoryStruct.comp (ψ.f i') (L.extendXIso e h).hom)
@[simp]
theorem
ComplexShape.Embedding.homRestrict.comm
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
(i j : ι)
:
CategoryTheory.CategoryStruct.comp (f ψ i) (L.d i j) = CategoryTheory.CategoryStruct.comp (K.d (e.f i) (e.f j)) (f ψ j)
@[simp]
theorem
ComplexShape.Embedding.homRestrict.comm_assoc
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
{e : c.Embedding c'}
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
(i j : ι)
{Z : C}
(h : L.X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (f ψ i) (CategoryTheory.CategoryStruct.comp (L.d i j) h) = CategoryTheory.CategoryStruct.comp (K.d (e.f i) (e.f j)) (CategoryTheory.CategoryStruct.comp (f ψ j) h)
noncomputable def
ComplexShape.Embedding.homRestrict
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
:
The morphism K.restriction e ⟶ L induced by a morphism K ⟶ L.extend e.
Equations
Instances For
theorem
ComplexShape.Embedding.homRestrict_f
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
{i : ι}
{i' : ι'}
(h : e.f i = i')
:
(e.homRestrict ψ).f i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e h).hom
(CategoryTheory.CategoryStruct.comp (ψ.f i') (L.extendXIso e h).hom)
theorem
ComplexShape.Embedding.homRestrict_hasLift
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
:
e.HasLift (e.homRestrict ψ)
@[simp]
theorem
ComplexShape.Embedding.liftExtend_homRestrict
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
:
@[simp]
theorem
ComplexShape.Embedding.homRestrict_liftExtend
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(φ : K.restriction e ⟶ L)
(hφ : e.HasLift φ)
:
theorem
ComplexShape.Embedding.homRestrict_precomp
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K K' : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(α : K' ⟶ K)
(ψ : K ⟶ L.extend e)
:
theorem
ComplexShape.Embedding.homRestrict_precomp_assoc
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K K' : HomologicalComplex C c'}
{L : HomologicalComplex C c}
[e.IsRelIff]
(α : K' ⟶ K)
(ψ : K ⟶ L.extend e)
{Z : HomologicalComplex C c}
(h : L ⟶ Z)
:
theorem
ComplexShape.Embedding.homRestrict_comp_extendMap
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L L' : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
(β : L ⟶ L')
:
theorem
ComplexShape.Embedding.homRestrict_comp_extendMap_assoc
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{K : HomologicalComplex C c'}
{L L' : HomologicalComplex C c}
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
(β : L ⟶ L')
{Z : HomologicalComplex C c}
(h : L' ⟶ Z)
:
noncomputable def
ComplexShape.Embedding.homEquiv
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c')
(L : HomologicalComplex C c)
[e.IsRelIff]
:
The bijection between K ⟶ L.extend e and the subtype of K.restriction e ⟶ L
consisting of morphisms φ such that e.HasLift φ.
Equations
Instances For
@[simp]
theorem
ComplexShape.Embedding.homEquiv_apply_coe
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c')
(L : HomologicalComplex C c)
[e.IsRelIff]
(ψ : K ⟶ L.extend e)
:
@[simp]
theorem
ComplexShape.Embedding.homEquiv_symm_apply
{ι : Type u_1}
{ι' : Type u_2}
{c : ComplexShape ι}
{c' : ComplexShape ι'}
(e : c.Embedding c')
{C : Type u_3}
[CategoryTheory.Category.{u_4, u_3} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
(K : HomologicalComplex C c')
(L : HomologicalComplex C c)
[e.IsRelIff]
(φ : { φ : K.restriction e ⟶ L // e.HasLift φ })
: