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) : Prop

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') : 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 φ) : 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') : 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) : 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)

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') : e.homRestrict (CategoryTheory.CategoryStruct.comp ψ (HomologicalComplex.extendMap β e)) = CategoryTheory.CategoryStruct.comp (e.homRestrict ψ) β

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) : CategoryTheory.CategoryStruct.comp (e.homRestrict (CategoryTheory.CategoryStruct.comp ψ (HomologicalComplex.extendMap β e))) h = CategoryTheory.CategoryStruct.comp (e.homRestrict ψ) (CategoryTheory.CategoryStruct.comp β 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] : (K ⟶ L.extend e) ≃ { φ : K.restriction e ⟶ L // e.HasLift φ }

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 ↑φ ⋯