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 #

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
      Instances For
        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

          The morphism K.restriction e ⟶ L induced by a morphism K ⟶ L.extend e.

          Equations
          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.
            Instances For