Documentation

Mathlib.Algebra.Homology.Embedding.HomEquiv

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 #

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' : ι') :
    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.
    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') :
      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_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) :
      @[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' : ι') :
      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
      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 φ ).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 φ ).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
        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') :
          CategoryTheory.IsIso ((e.liftExtend φ ).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 φ ).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 φ ).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
          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') :
            ComplexShape.Embedding.homRestrict.f ψ i = CategoryTheory.CategoryStruct.comp (K.restrictionXIso e h).hom (CategoryTheory.CategoryStruct.comp (ψ.f i') (L.extendXIso e h).hom)
            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
            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) :
              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 φ ) = φ
              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 : HomologicalComplex C c'} {K' : HomologicalComplex C c'} {L : HomologicalComplex C c} [e.IsRelIff] (α : K' K) (ψ : 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 φ }) :
              (e.homEquiv K L).symm φ = e.liftExtend φ
              @[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 ψ
              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.
              Instances For