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
- e.HasLift φ = ∀ (j : ι), e.BoundaryGE j → ∀ (i' : ι'), c'.Rel i' (e.f j) → CategoryTheory.CategoryStruct.comp (K.d i' (e.f j)) (φ.f j) = 0
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' : ι')
:
K.X i' ⟶ (L.extend e).X i'
Auxiliary definition for liftExtend.
Equations
- One or more equations did not get rendered due to their size.
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')
:
ComplexShape.Embedding.liftExtend.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 (ComplexShape.Embedding.liftExtend.f φ i') ((L.extend e).d i' j') = CategoryTheory.CategoryStruct.comp (K.d i' j') (ComplexShape.Embedding.liftExtend.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 (ComplexShape.Embedding.liftExtend.f φ i')
(CategoryTheory.CategoryStruct.comp ((L.extend e).d i' j') h) = CategoryTheory.CategoryStruct.comp (K.d i' j')
(CategoryTheory.CategoryStruct.comp (ComplexShape.Embedding.liftExtend.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 φ)
:
K ⟶ L.extend e
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' := ⋯ }
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')
:
CategoryTheory.Arrow.mk ((e.liftExtend φ hφ).f i') ≅ CategoryTheory.Arrow.mk (φ.f 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
- e.liftExtendfArrowIso φ hφ hi = CategoryTheory.Arrow.isoMk (K.restrictionXIso e hi).symm (L.extendXIso e hi) ⋯
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')
:
CategoryTheory.IsIso ((e.liftExtend φ hφ).f i') ↔ CategoryTheory.IsIso (φ.f 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')
:
CategoryTheory.Mono ((e.liftExtend φ hφ).f i') ↔ CategoryTheory.Mono (φ.f 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')
:
CategoryTheory.Epi ((e.liftExtend φ hφ).f i') ↔ CategoryTheory.Epi (φ.f 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 : ι)
:
(K.restriction e).X i ⟶ L.X i
Auxiliary definition for Embedding.homRestrict.
Equations
- ComplexShape.Embedding.homRestrict.f ψ i = CategoryTheory.CategoryStruct.comp (ψ.f (e.f i)) (L.extendXIso e ⋯).hom
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')
:
ComplexShape.Embedding.homRestrict.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 (ComplexShape.Embedding.homRestrict.f ψ i) (L.d i j) = CategoryTheory.CategoryStruct.comp (K.d (e.f i) (e.f j)) (ComplexShape.Embedding.homRestrict.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 (ComplexShape.Embedding.homRestrict.f ψ i)
(CategoryTheory.CategoryStruct.comp (L.d i j) h) = CategoryTheory.CategoryStruct.comp (K.d (e.f i) (e.f j))
(CategoryTheory.CategoryStruct.comp (ComplexShape.Embedding.homRestrict.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)
:
K.restriction e ⟶ L
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' := ⋯ }
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)
:
e.liftExtend (e.homRestrict ψ) ⋯ = ψ
@[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 φ)
:
e.homRestrict (e.liftExtend φ hφ) = φ
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)
:
e.homRestrict (CategoryTheory.CategoryStruct.comp α ψ) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap α e) (e.homRestrict ψ)
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)
:
CategoryTheory.CategoryStruct.comp (e.homRestrict (CategoryTheory.CategoryStruct.comp α ψ)) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.restrictionMap α e)
(CategoryTheory.CategoryStruct.comp (e.homRestrict ψ) h)
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
- One or more equations did not get rendered due to their size.
@[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)
:
↑((e.homEquiv K L) ψ) = e.homRestrict ψ
@[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 φ })
:
(e.homEquiv K L).symm φ = e.liftExtend ↑φ ⋯