Library UniMath.CategoryTheory.FiveLemma
FiveLemma
Contents
- Definition of structures for five lemma
- Five Lemma structure to opposite category
- Five Lemma
- Five Lemma for short exact sequences, ShortExact
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.CategoryTheory.limits.zero.
Require Import UniMath.CategoryTheory.limits.pushouts.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.limits.equalizers.
Require Import UniMath.CategoryTheory.limits.coequalizers.
Require Import UniMath.CategoryTheory.limits.Opp.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.opp_precat.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.Morphisms.
Require Import UniMath.CategoryTheory.CategoriesWithBinOps.
Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops.
Require Import UniMath.CategoryTheory.PreAdditive.
Require Import UniMath.CategoryTheory.Additive.
Require Import UniMath.CategoryTheory.Abelian.
Require Import UniMath.CategoryTheory.AbelianToAdditive.
Require Import UniMath.CategoryTheory.AbelianPushoutPullback.
Require Import UniMath.CategoryTheory.ShortExactSequences.
Require Import UniMath.CategoryTheory.PseudoElements.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.limits.kernels.
Require Import UniMath.CategoryTheory.limits.cokernels.
Require Import UniMath.CategoryTheory.limits.BinDirectSums.
FiveLemma
Five lemma says that if you have the following commutative diagram in an abelian category C_1 --> C_2 --> C_3 --> C_4 --> C_5 f_1 | f_2 | f_3 | f_4 | f_5 | D_1 --> D_2 --> D_3 --> D_4 --> D_5 where the rows are exact and the morphisms f_1, f_2, f_4, and f_5 are isomorphisms, then f_3 is an isomorphism. Exactness of the first row means that an image of C_1 --> C_2 is a kernel of C_2 --> C_3, an image of C_2 --> C_3 is a kernel of C_3 --> C_4, and an image of C_3 --> C_4 is a kernel of C_4 --> C_5.Introduction
In this section we define the data needed to state the five lemma. The main definitions are FiveRow and FiveRowMorphism. The first contains the data of a row in the five lemma, and the second contains the data for a morphism between two rows.Definition FiveRowObs : UU := (ob A) × (ob A) × (ob A) × (ob A) × (ob A).
Definition make_FiveRowObs (C1 C2 C3 C4 C5 : ob A) : FiveRowObs := (C1,,(C2,,(C3,,(C4,,C5)))).
Definition FOb1 (FRO : FiveRowObs) : ob A := dirprod_pr1 FRO.
Definition FOb2 (FRO : FiveRowObs) : ob A := dirprod_pr1 (dirprod_pr2 FRO).
Definition FOb3 (FRO : FiveRowObs) : ob A := dirprod_pr1 (dirprod_pr2 (dirprod_pr2 FRO)).
Definition FOb4 (FRO : FiveRowObs) : ob A :=
dirprod_pr1 (dirprod_pr2 (dirprod_pr2 (dirprod_pr2 FRO))).
Definition FOb5 (FRO : FiveRowObs) : ob A :=
dirprod_pr2 (dirprod_pr2 (dirprod_pr2 (dirprod_pr2 FRO))).
Definition FiveRowDiffs (FRO : FiveRowObs) : UU :=
(A⟦FOb1 FRO, FOb2 FRO⟧) × (A⟦FOb2 FRO, FOb3 FRO⟧) × (A⟦FOb3 FRO, FOb4 FRO⟧)
× (A⟦FOb4 FRO, FOb5 FRO⟧).
Definition make_FiveRowDiffs (FRO : FiveRowObs) (f1 : A⟦FOb1 FRO, FOb2 FRO⟧)
(f2 : A⟦FOb2 FRO, FOb3 FRO⟧) (f3 : A⟦FOb3 FRO, FOb4 FRO⟧)
(f4 : A⟦FOb4 FRO, FOb5 FRO⟧) : FiveRowDiffs FRO := (f1,,(f2,,(f3,,f4))).
Definition FDiff1 {FRO : FiveRowObs} (FRD : FiveRowDiffs FRO) : A⟦FOb1 FRO, FOb2 FRO⟧ :=
dirprod_pr1 FRD.
Definition FDiff2 {FRO : FiveRowObs} (FRD : FiveRowDiffs FRO) : A⟦FOb2 FRO, FOb3 FRO⟧ :=
dirprod_pr1 (dirprod_pr2 FRD).
Definition FDiff3 {FRO : FiveRowObs} (FRD : FiveRowDiffs FRO) : A⟦FOb3 FRO, FOb4 FRO⟧ :=
dirprod_pr1 (dirprod_pr2 (dirprod_pr2 FRD)).
Definition FDiff4 {FRO : FiveRowObs} (FRD : FiveRowDiffs FRO) : A⟦FOb4 FRO, FOb5 FRO⟧ :=
dirprod_pr2 (dirprod_pr2 (dirprod_pr2 FRD)).
Definition FiveRowDiffsEq {FRO : FiveRowObs} (FRD : FiveRowDiffs FRO) : UU :=
(FDiff1 FRD · FDiff2 FRD = ZeroArrow (to_Zero A) _ _)
× (FDiff2 FRD · FDiff3 FRD = ZeroArrow (to_Zero A) _ _)
× (FDiff3 FRD · FDiff4 FRD = ZeroArrow (to_Zero A) _ _).
Definition make_FiveRowDiffsEq {FRO : FiveRowObs} (FRD : FiveRowDiffs FRO)
(H1 : FDiff1 FRD · FDiff2 FRD = ZeroArrow (to_Zero A) _ _)
(H2 : FDiff2 FRD · FDiff3 FRD = ZeroArrow (to_Zero A) _ _)
(H3 : FDiff3 FRD · FDiff4 FRD = ZeroArrow (to_Zero A) _ _) : FiveRowDiffsEq FRD :=
(H1,,(H2,,H3)).
Definition FEq1 {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO} (FRDE : FiveRowDiffsEq FRD) :
FDiff1 FRD · FDiff2 FRD = ZeroArrow (to_Zero A) _ _ := dirprod_pr1 FRDE.
Definition FEq2 {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO} (FRDE : FiveRowDiffsEq FRD) :
FDiff2 FRD · FDiff3 FRD = ZeroArrow (to_Zero A) _ _ := dirprod_pr1 (dirprod_pr2 FRDE).
Definition FEq3 {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO} (FRDE : FiveRowDiffsEq FRD) :
FDiff3 FRD · FDiff4 FRD = ZeroArrow (to_Zero A) _ _ := dirprod_pr2 (dirprod_pr2 FRDE).
Definition FiveRowExacts {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO}
(FRDE : FiveRowDiffsEq FRD) : UU :=
(isExact A (FDiff1 FRD) (FDiff2 FRD) (FEq1 FRDE))
× (isExact A (FDiff2 FRD) (FDiff3 FRD) (FEq2 FRDE))
× (isExact A (FDiff3 FRD) (FDiff4 FRD) (FEq3 FRDE)).
Definition make_FiveRowExacts {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO}
(FRDE : FiveRowDiffsEq FRD) (H1 : isExact A (FDiff1 FRD) (FDiff2 FRD) (FEq1 FRDE))
(H2 : isExact A (FDiff2 FRD) (FDiff3 FRD) (FEq2 FRDE))
(H3 : isExact A (FDiff3 FRD) (FDiff4 FRD) (FEq3 FRDE)) : FiveRowExacts FRDE :=
(H1,,(H2,,H3)).
Definition FEx1 {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO} {FRDE : FiveRowDiffsEq FRD}
(FRE : FiveRowExacts FRDE) : isExact A (FDiff1 FRD) (FDiff2 FRD) (FEq1 FRDE) :=
dirprod_pr1 FRE.
Definition FEx2 {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO} {FRDE : FiveRowDiffsEq FRD}
(FRE : FiveRowExacts FRDE) : isExact A (FDiff2 FRD) (FDiff3 FRD) (FEq2 FRDE) :=
dirprod_pr1 (dirprod_pr2 FRE).
Definition FEx3 {FRO : FiveRowObs} {FRD : FiveRowDiffs FRO} {FRDE : FiveRowDiffsEq FRD}
(FRE : FiveRowExacts FRDE) : isExact A (FDiff3 FRD) (FDiff4 FRD) (FEq3 FRDE) :=
dirprod_pr2 (dirprod_pr2 FRE).
Define row for FiveLemma
Definition FiveRow : UU :=
∑ (FRO : FiveRowObs),
(∑ (FRD : FiveRowDiffs FRO), (∑ (FRDE : FiveRowDiffsEq FRD), FiveRowExacts FRDE)).
Definition make_FiveRow (FRO : FiveRowObs) (FRD : FiveRowDiffs FRO) (FRDE : FiveRowDiffsEq FRD)
(FRE : FiveRowExacts FRDE) : FiveRow := (FRO,,(FRD,,(FRDE,,FRE))).
Definition FiveRow_Obs (FR : FiveRow) : FiveRowObs := pr1 FR.
Coercion FiveRow_Obs : FiveRow >-> FiveRowObs.
Definition FiveRow_Diffs (FR : FiveRow) : FiveRowDiffs FR := pr1 (pr2 FR).
Coercion FiveRow_Diffs : FiveRow >-> FiveRowDiffs.
Definition FiveRow_DiffsEq (FR : FiveRow) : FiveRowDiffsEq FR := pr1 (pr2 (pr2 FR)).
Coercion FiveRow_DiffsEq : FiveRow >-> FiveRowDiffsEq.
Definition FiveRow_Exacts (FR : FiveRow) : FiveRowExacts FR := pr2 (pr2 (pr2 FR)).
Coercion FiveRow_Exacts : FiveRow >-> FiveRowExacts.
Definition FiveRowMors (FR1 FR2 : FiveRow) : UU :=
(A⟦FOb1 FR1, FOb1 FR2⟧) × (A⟦FOb2 FR1, FOb2 FR2⟧) × (A⟦FOb3 FR1, FOb3 FR2⟧)
× (A⟦FOb4 FR1, FOb4 FR2⟧) × (A⟦FOb5 FR1, FOb5 FR2⟧).
Definition make_FiveRowMors (FR1 FR2 : FiveRow) (f1 : A⟦FOb1 FR1, FOb1 FR2⟧)
(f2 : A⟦FOb2 FR1, FOb2 FR2⟧) (f3 : A⟦FOb3 FR1, FOb3 FR2⟧)
(f4 : A⟦FOb4 FR1, FOb4 FR2⟧) (f5 : A⟦FOb5 FR1, FOb5 FR2⟧) : FiveRowMors FR1 FR2 :=
(f1,,(f2,,(f3,,(f4,,f5)))).
Definition FMor1 {FR1 FR2 : FiveRow} (FRMs : FiveRowMors FR1 FR2) : A⟦FOb1 FR1, FOb1 FR2⟧ :=
dirprod_pr1 FRMs.
Definition FMor2 {FR1 FR2 : FiveRow} (FRMs : FiveRowMors FR1 FR2) : A⟦FOb2 FR1, FOb2 FR2⟧ :=
dirprod_pr1 (dirprod_pr2 FRMs).
Definition FMor3 {FR1 FR2 : FiveRow} (FRMs : FiveRowMors FR1 FR2) : A⟦FOb3 FR1, FOb3 FR2⟧ :=
dirprod_pr1 (dirprod_pr2 (dirprod_pr2 FRMs)).
Definition FMor4 {FR1 FR2 : FiveRow} (FRMs : FiveRowMors FR1 FR2) : A⟦FOb4 FR1, FOb4 FR2⟧ :=
dirprod_pr1 (dirprod_pr2 (dirprod_pr2 (dirprod_pr2 FRMs))).
Definition FMor5 {FR1 FR2 : FiveRow} (FRMs : FiveRowMors FR1 FR2) : A⟦FOb5 FR1, FOb5 FR2⟧ :=
dirprod_pr2 (dirprod_pr2 (dirprod_pr2 (dirprod_pr2 FRMs))).
Definition FiveRowMorsComm {FR1 FR2 : FiveRow} (FRMs : FiveRowMors FR1 FR2) : UU :=
(FDiff1 FR1 · FMor2 FRMs = FMor1 FRMs · FDiff1 FR2)
× (FDiff2 FR1 · FMor3 FRMs = FMor2 FRMs · FDiff2 FR2)
× (FDiff3 FR1 · FMor4 FRMs = FMor3 FRMs · FDiff3 FR2)
× (FDiff4 FR1 · FMor5 FRMs = FMor4 FRMs · FDiff4 FR2).
Definition make_FiveRowMorsComm {FR1 FR2 : FiveRow} (FRMs : FiveRowMors FR1 FR2)
(H1 : FDiff1 FR1 · FMor2 FRMs = FMor1 FRMs · FDiff1 FR2)
(H2 : FDiff2 FR1 · FMor3 FRMs = FMor2 FRMs · FDiff2 FR2)
(H3 : FDiff3 FR1 · FMor4 FRMs = FMor3 FRMs · FDiff3 FR2)
(H4 : FDiff4 FR1 · FMor5 FRMs = FMor4 FRMs · FDiff4 FR2) : FiveRowMorsComm FRMs :=
(H1,,(H2,,(H3,,H4))).
Definition FComm1 {FR1 FR2 : FiveRow} {FRMs : FiveRowMors FR1 FR2} (FRMC : FiveRowMorsComm FRMs) :
FDiff1 FR1 · FMor2 FRMs = FMor1 FRMs · FDiff1 FR2 := dirprod_pr1 FRMC.
Definition FComm2 {FR1 FR2 : FiveRow} {FRMs : FiveRowMors FR1 FR2} (FRMC : FiveRowMorsComm FRMs) :
FDiff2 FR1 · FMor3 FRMs = FMor2 FRMs · FDiff2 FR2 := dirprod_pr1 (dirprod_pr2 FRMC).
Definition FComm3 {FR1 FR2 : FiveRow} {FRMs : FiveRowMors FR1 FR2} (FRMC : FiveRowMorsComm FRMs) :
FDiff3 FR1 · FMor4 FRMs = FMor3 FRMs · FDiff3 FR2 :=
dirprod_pr1 (dirprod_pr2 (dirprod_pr2 FRMC)).
Definition FComm4 {FR1 FR2 : FiveRow} {FRMs : FiveRowMors FR1 FR2} (FRMC : FiveRowMorsComm FRMs) :
FDiff4 FR1 · FMor5 FRMs = FMor4 FRMs · FDiff4 FR2 :=
dirprod_pr2 (dirprod_pr2 (dirprod_pr2 FRMC)).
Definition FiveRowMorphism (FR1 FR2 : FiveRow) : UU :=
∑ (FRMs : FiveRowMors FR1 FR2), FiveRowMorsComm FRMs.
Definition make_FiveRowMorphism (FR1 FR2 : FiveRow) (FRMs : FiveRowMors FR1 FR2)
(FRMC : FiveRowMorsComm FRMs) : FiveRowMorphism FR1 FR2 := (FRMs,,FRMC).
Definition FiveRowMorphism_Mors {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2) :
FiveRowMors FR1 FR2 := pr1 FRM.
Coercion FiveRowMorphism_Mors : FiveRowMorphism >-> FiveRowMors.
Definition FiveRowMorphism_Comms {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2) :
FiveRowMorsComm FRM := pr2 FRM.
Coercion FiveRowMorphism_Comms : FiveRowMorphism >-> FiveRowMorsComm.
End five_lemma_data.
Introduction
In this section we translate the definitions in the previous section five_lemma_data to opposite categories, so that FiveLemma_isEpi can use these.
Section five_lemma_opp.
Definition FiveRowObs_opp {A : AbelianPreCat} (FRO : FiveRowObs) :
@FiveRowObs (Abelian_opp A) :=
@make_FiveRowObs (Abelian_opp A) (FOb5 FRO) (FOb4 FRO) (FOb3 FRO) (FOb2 FRO) (FOb1 FRO).
Definition FiveRowDiffs_opp {A : AbelianPreCat} {FRO : @FiveRowObs A}
(FRD : FiveRowDiffs FRO) : @FiveRowDiffs (Abelian_opp A) (FiveRowObs_opp FRO) :=
@make_FiveRowDiffs (Abelian_opp A) (FiveRowObs_opp FRO)
(FDiff4 FRD) (FDiff3 FRD) (FDiff2 FRD) (FDiff1 FRD).
Local Opaque ZeroArrow.
Local Lemma FiveRowDiffsEq_opp1 {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
(@FDiff1 (Abelian_opp A) _ (FiveRowDiffs_opp FRD))
· (@FDiff2 (Abelian_opp A) _ (FiveRowDiffs_opp FRD)) =
ZeroArrow (to_Zero (Abelian_opp A)) _ _.
Show proof.
Local Lemma FiveRowDiffsEq_opp2 {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
(@FDiff2 (Abelian_opp A) _ (FiveRowDiffs_opp FRD))
· (@FDiff3 (Abelian_opp A) _ (FiveRowDiffs_opp FRD)) =
ZeroArrow (to_Zero (Abelian_opp A)) _ _.
Show proof.
Local Lemma FiveRowDiffsEq_opp3 {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
(@FDiff3 (Abelian_opp A) _ (FiveRowDiffs_opp FRD))
· (@FDiff4 (Abelian_opp A) _ (FiveRowDiffs_opp FRD)) =
ZeroArrow (to_Zero (Abelian_opp A)) _ _.
Show proof.
Definition FiveRowDiffsEq_opp {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
@FiveRowDiffsEq (Abelian_opp A) _ (FiveRowDiffs_opp FRD) :=
@make_FiveRowDiffsEq _ _ (FiveRowDiffs_opp FRD) (FiveRowDiffsEq_opp1 FRDE)
(FiveRowDiffsEq_opp2 FRDE) (FiveRowDiffsEq_opp3 FRDE).
Definition FiveRowExacts_opp {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} {FRDE : @FiveRowDiffsEq A FRO FRD}
(FRE : @FiveRowExacts A FRO FRD FRDE) :
@FiveRowExacts (Abelian_opp A) _ _ (FiveRowDiffsEq_opp FRDE) :=
@make_FiveRowExacts (Abelian_opp A) _ _ (FiveRowDiffsEq_opp FRDE)
(isExact_opp (FEx3 FRE)) (isExact_opp (FEx2 FRE))
(isExact_opp (FEx1 FRE)).
Definition FiveRow_opp {A : AbelianPreCat} (FR : @FiveRow A) :
@FiveRow (Abelian_opp A) :=
@make_FiveRow (Abelian_opp A) (FiveRowObs_opp FR)
(FiveRowDiffs_opp FR) (FiveRowDiffsEq_opp FR) (FiveRowExacts_opp FR).
Definition FiveRowMors_opp {A : AbelianPreCat} {FR1 FR2 : @FiveRow A}
(FRM : @FiveRowMors A FR1 FR2) :
@FiveRowMors (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1) :=
@make_FiveRowMors (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1)
(FMor5 FRM) (FMor4 FRM) (FMor3 FRM) (FMor2 FRM) (FMor1 FRM).
Definition FiveRowMorsComm_opp {A : AbelianPreCat} {FR1 FR2 : @FiveRow A}
{FRM : @FiveRowMors A FR1 FR2} (FRMC : @FiveRowMorsComm A FR1 FR2 FRM) :
@FiveRowMorsComm (Abelian_opp A) _ _ (FiveRowMors_opp FRM) :=
@make_FiveRowMorsComm (Abelian_opp A) _ _ (FiveRowMors_opp FRM)
(! FComm4 FRMC) (! FComm3 FRMC) (! FComm2 FRMC) (! FComm1 FRMC).
Definition FiveRowMorphism_opp {A : AbelianPreCat} {FR1 FR2 : @FiveRow A}
(FRM : @FiveRowMorphism A FR1 FR2) :
@FiveRowMorphism (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1) :=
@make_FiveRowMorphism (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1)
(FiveRowMors_opp FRM) (FiveRowMorsComm_opp FRM).
End five_lemma_opp.
Definition FiveRowObs_opp {A : AbelianPreCat} (FRO : FiveRowObs) :
@FiveRowObs (Abelian_opp A) :=
@make_FiveRowObs (Abelian_opp A) (FOb5 FRO) (FOb4 FRO) (FOb3 FRO) (FOb2 FRO) (FOb1 FRO).
Definition FiveRowDiffs_opp {A : AbelianPreCat} {FRO : @FiveRowObs A}
(FRD : FiveRowDiffs FRO) : @FiveRowDiffs (Abelian_opp A) (FiveRowObs_opp FRO) :=
@make_FiveRowDiffs (Abelian_opp A) (FiveRowObs_opp FRO)
(FDiff4 FRD) (FDiff3 FRD) (FDiff2 FRD) (FDiff1 FRD).
Local Opaque ZeroArrow.
Local Lemma FiveRowDiffsEq_opp1 {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
(@FDiff1 (Abelian_opp A) _ (FiveRowDiffs_opp FRD))
· (@FDiff2 (Abelian_opp A) _ (FiveRowDiffs_opp FRD)) =
ZeroArrow (to_Zero (Abelian_opp A)) _ _.
Show proof.
Local Lemma FiveRowDiffsEq_opp2 {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
(@FDiff2 (Abelian_opp A) _ (FiveRowDiffs_opp FRD))
· (@FDiff3 (Abelian_opp A) _ (FiveRowDiffs_opp FRD)) =
ZeroArrow (to_Zero (Abelian_opp A)) _ _.
Show proof.
Local Lemma FiveRowDiffsEq_opp3 {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
(@FDiff3 (Abelian_opp A) _ (FiveRowDiffs_opp FRD))
· (@FDiff4 (Abelian_opp A) _ (FiveRowDiffs_opp FRD)) =
ZeroArrow (to_Zero (Abelian_opp A)) _ _.
Show proof.
Definition FiveRowDiffsEq_opp {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} (FRDE : @FiveRowDiffsEq A FRO FRD) :
@FiveRowDiffsEq (Abelian_opp A) _ (FiveRowDiffs_opp FRD) :=
@make_FiveRowDiffsEq _ _ (FiveRowDiffs_opp FRD) (FiveRowDiffsEq_opp1 FRDE)
(FiveRowDiffsEq_opp2 FRDE) (FiveRowDiffsEq_opp3 FRDE).
Definition FiveRowExacts_opp {A : AbelianPreCat} {FRO : @FiveRowObs A}
{FRD : @FiveRowDiffs A FRO} {FRDE : @FiveRowDiffsEq A FRO FRD}
(FRE : @FiveRowExacts A FRO FRD FRDE) :
@FiveRowExacts (Abelian_opp A) _ _ (FiveRowDiffsEq_opp FRDE) :=
@make_FiveRowExacts (Abelian_opp A) _ _ (FiveRowDiffsEq_opp FRDE)
(isExact_opp (FEx3 FRE)) (isExact_opp (FEx2 FRE))
(isExact_opp (FEx1 FRE)).
Definition FiveRow_opp {A : AbelianPreCat} (FR : @FiveRow A) :
@FiveRow (Abelian_opp A) :=
@make_FiveRow (Abelian_opp A) (FiveRowObs_opp FR)
(FiveRowDiffs_opp FR) (FiveRowDiffsEq_opp FR) (FiveRowExacts_opp FR).
Definition FiveRowMors_opp {A : AbelianPreCat} {FR1 FR2 : @FiveRow A}
(FRM : @FiveRowMors A FR1 FR2) :
@FiveRowMors (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1) :=
@make_FiveRowMors (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1)
(FMor5 FRM) (FMor4 FRM) (FMor3 FRM) (FMor2 FRM) (FMor1 FRM).
Definition FiveRowMorsComm_opp {A : AbelianPreCat} {FR1 FR2 : @FiveRow A}
{FRM : @FiveRowMors A FR1 FR2} (FRMC : @FiveRowMorsComm A FR1 FR2 FRM) :
@FiveRowMorsComm (Abelian_opp A) _ _ (FiveRowMors_opp FRM) :=
@make_FiveRowMorsComm (Abelian_opp A) _ _ (FiveRowMors_opp FRM)
(! FComm4 FRMC) (! FComm3 FRMC) (! FComm2 FRMC) (! FComm1 FRMC).
Definition FiveRowMorphism_opp {A : AbelianPreCat} {FR1 FR2 : @FiveRow A}
(FRM : @FiveRowMorphism A FR1 FR2) :
@FiveRowMorphism (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1) :=
@make_FiveRowMorphism (Abelian_opp A) (FiveRow_opp FR2) (FiveRow_opp FR1)
(FiveRowMors_opp FRM) (FiveRowMorsComm_opp FRM).
End five_lemma_opp.
Introduction
In this section we prove the five lemma following the sketch of a proof on top of this file.
Section five_lemma.
Lemma FiveLemma_isMonic {A : AbelianPreCat} {FR1 FR2 : FiveRow}
(FRM : FiveRowMorphism FR1 FR2) (H1 : is_z_isomorphism (FMor1 FRM))
(H2 : is_z_isomorphism (FMor2 FRM)) (H4 : is_z_isomorphism (FMor4 FRM))
(H5 : is_z_isomorphism (FMor5 FRM)) : isMonic (FMor3 (A:=A) FRM).
Show proof.
Context {A : AbelianPreCat}.
Lemma FiveLemma_isEpi {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2)
(H1 : is_z_isomorphism (FMor1 FRM)) (H2 : is_z_isomorphism (FMor2 FRM))
(H4 : is_z_isomorphism (FMor4 FRM)) (H5 : is_z_isomorphism (FMor5 FRM)) :
isEpi (FMor3 (A:=A) FRM).
Show proof.
Lemma FiveLemma {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2)
(H1 : is_z_isomorphism (FMor1 FRM)) (H2 : is_z_isomorphism (FMor2 FRM))
(H4 : is_z_isomorphism (FMor4 FRM)) (H5 : is_z_isomorphism (FMor5 FRM)) :
is_z_isomorphism (FMor3 (A:=A) FRM).
Show proof.
End five_lemma.
Lemma FiveLemma_isMonic {A : AbelianPreCat} {FR1 FR2 : FiveRow}
(FRM : FiveRowMorphism FR1 FR2) (H1 : is_z_isomorphism (FMor1 FRM))
(H2 : is_z_isomorphism (FMor2 FRM)) (H4 : is_z_isomorphism (FMor4 FRM))
(H5 : is_z_isomorphism (FMor5 FRM)) : isMonic (FMor3 (A:=A) FRM).
Show proof.
use (dirprod_pr2 (PEq_isMonic (FMor3 FRM))).
intros d' a X. apply pathsinv0. cbn in X. set (X' := PEq_Zero_Eq' _ _ X). cbn in X'.
assert (e1 : a · FDiff3 FR1 = ZeroArrow (to_Zero A) _ _).
{
set (comm := FComm3 FRM). use (is_iso_isMonic A _ H4).
rewrite <- assoc. rewrite comm. clear comm. rewrite assoc.
rewrite X'. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left.
apply idpath.
}
set (b := dirprod_pr1 (PEq_isExact _ _ (FEq2 FR1)) (FEx2 FR1) a e1).
set (PE1 := PseudoIm b (FMor2 FRM)).
assert (e2 : PE1 · FDiff2 FR2 = ZeroArrow (to_Zero A) _ _).
{
cbn. set (comm := FComm2 FRM). rewrite <- assoc. rewrite <- comm. clear comm.
rewrite assoc. set (tmp := PEqEq (PFiber_Eq b)). cbn in tmp.
use (EpiisEpi _ (PEqEpi2 (PFiber_Eq b))). rewrite assoc.
cbn in tmp. cbn. rewrite <- tmp. clear tmp. rewrite <- assoc. rewrite X'.
rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right.
apply idpath.
}
set (b' := dirprod_pr1 (PEq_isExact _ _ (FEq1 FR2)) (FEx1 FR2) PE1 e2).
set (a' := dirprod_pr1 (PEq_isEpi (FMor1 FRM)) (is_iso_isEpi A _ H1) b').
assert (e3 : PEq (PseudoIm a' (FDiff1 FR1)) b).
{
assert (e31 : PEq (PseudoIm (PseudoIm a' (FDiff1 FR1)) (FMor2 FRM))
(PseudoIm b (FMor2 FRM))).
{
use (PEq_trans (PEq_Im_Comm a' (FComm1 FRM))).
use (PEq_trans (PEq_Im _ _ (FDiff1 FR2) (PFiber_Eq a'))).
use (PEq_trans (PFiber_Eq b')). use PEq_refl.
}
exact (dirprod_pr1 (PEq_isMonic' (FMor2 FRM)) (is_iso_isMonic A _ H2)
(PseudoIm a' (FDiff1 FR1)) b e31).
}
assert (e4 : PEq (PseudoIm (PseudoIm a' (FDiff1 FR1)) (FDiff2 FR1)) a).
{
use (PEq_trans _ (PFiber_Eq b)).
use (PEq_trans _ (PEq_Im _ _ (FDiff2 FR1) e3)).
use PEq_refl.
}
use PEq_Zero_Eq'.
- exact (PseudoOb a').
- use (PEq_trans (PEq_symm e4)).
use (PEq_trans (PEq_Comp a' (FDiff1 FR1) (FDiff2 FR1))).
use (PEq_trans (PEq_Im_Paths a' (FEq1 FR1))).
use PEq_Eq_Zero. cbn. apply ZeroArrow_comp_right.
intros d' a X. apply pathsinv0. cbn in X. set (X' := PEq_Zero_Eq' _ _ X). cbn in X'.
assert (e1 : a · FDiff3 FR1 = ZeroArrow (to_Zero A) _ _).
{
set (comm := FComm3 FRM). use (is_iso_isMonic A _ H4).
rewrite <- assoc. rewrite comm. clear comm. rewrite assoc.
rewrite X'. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_left.
apply idpath.
}
set (b := dirprod_pr1 (PEq_isExact _ _ (FEq2 FR1)) (FEx2 FR1) a e1).
set (PE1 := PseudoIm b (FMor2 FRM)).
assert (e2 : PE1 · FDiff2 FR2 = ZeroArrow (to_Zero A) _ _).
{
cbn. set (comm := FComm2 FRM). rewrite <- assoc. rewrite <- comm. clear comm.
rewrite assoc. set (tmp := PEqEq (PFiber_Eq b)). cbn in tmp.
use (EpiisEpi _ (PEqEpi2 (PFiber_Eq b))). rewrite assoc.
cbn in tmp. cbn. rewrite <- tmp. clear tmp. rewrite <- assoc. rewrite X'.
rewrite ZeroArrow_comp_right. rewrite ZeroArrow_comp_right.
apply idpath.
}
set (b' := dirprod_pr1 (PEq_isExact _ _ (FEq1 FR2)) (FEx1 FR2) PE1 e2).
set (a' := dirprod_pr1 (PEq_isEpi (FMor1 FRM)) (is_iso_isEpi A _ H1) b').
assert (e3 : PEq (PseudoIm a' (FDiff1 FR1)) b).
{
assert (e31 : PEq (PseudoIm (PseudoIm a' (FDiff1 FR1)) (FMor2 FRM))
(PseudoIm b (FMor2 FRM))).
{
use (PEq_trans (PEq_Im_Comm a' (FComm1 FRM))).
use (PEq_trans (PEq_Im _ _ (FDiff1 FR2) (PFiber_Eq a'))).
use (PEq_trans (PFiber_Eq b')). use PEq_refl.
}
exact (dirprod_pr1 (PEq_isMonic' (FMor2 FRM)) (is_iso_isMonic A _ H2)
(PseudoIm a' (FDiff1 FR1)) b e31).
}
assert (e4 : PEq (PseudoIm (PseudoIm a' (FDiff1 FR1)) (FDiff2 FR1)) a).
{
use (PEq_trans _ (PFiber_Eq b)).
use (PEq_trans _ (PEq_Im _ _ (FDiff2 FR1) e3)).
use PEq_refl.
}
use PEq_Zero_Eq'.
- exact (PseudoOb a').
- use (PEq_trans (PEq_symm e4)).
use (PEq_trans (PEq_Comp a' (FDiff1 FR1) (FDiff2 FR1))).
use (PEq_trans (PEq_Im_Paths a' (FEq1 FR1))).
use PEq_Eq_Zero. cbn. apply ZeroArrow_comp_right.
Context {A : AbelianPreCat}.
Lemma FiveLemma_isEpi {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2)
(H1 : is_z_isomorphism (FMor1 FRM)) (H2 : is_z_isomorphism (FMor2 FRM))
(H4 : is_z_isomorphism (FMor4 FRM)) (H5 : is_z_isomorphism (FMor5 FRM)) :
isEpi (FMor3 (A:=A) FRM).
Show proof.
use opp_isMonic.
set (H1' := opp_is_z_isomorphism _ H1).
set (H2' := opp_is_z_isomorphism _ H2).
set (H4' := opp_is_z_isomorphism _ H4).
set (H5' := opp_is_z_isomorphism _ H5).
set (FRM' := FiveRowMorphism_opp FRM).
exact (FiveLemma_isMonic FRM' H5' H4' H2' H1').
set (H1' := opp_is_z_isomorphism _ H1).
set (H2' := opp_is_z_isomorphism _ H2).
set (H4' := opp_is_z_isomorphism _ H4).
set (H5' := opp_is_z_isomorphism _ H5).
set (FRM' := FiveRowMorphism_opp FRM).
exact (FiveLemma_isMonic FRM' H5' H4' H2' H1').
Lemma FiveLemma {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2)
(H1 : is_z_isomorphism (FMor1 FRM)) (H2 : is_z_isomorphism (FMor2 FRM))
(H4 : is_z_isomorphism (FMor4 FRM)) (H5 : is_z_isomorphism (FMor5 FRM)) :
is_z_isomorphism (FMor3 (A:=A) FRM).
Show proof.
use monic_epi_is_iso.
- use FiveLemma_isMonic.
+ exact H1.
+ exact H2.
+ exact H4.
+ exact H5.
- use FiveLemma_isEpi.
+ exact H1.
+ exact H2.
+ exact H4.
+ exact H5.
- use FiveLemma_isMonic.
+ exact H1.
+ exact H2.
+ exact H4.
+ exact H5.
- use FiveLemma_isEpi.
+ exact H1.
+ exact H2.
+ exact H4.
+ exact H5.
End five_lemma.
Introduction
Five lemma for short exact sequences. Suppose you have a morphism of short exact sequences represented by the following diagram 0 --> C_1 --> C_2 --> C_3 --> 0 | f_2 | f_3 | f_4 | | 0 --> D_1 --> D_2 --> D_3 --> 0 If f_2 and f_4 are isomorphisms, then f_3 is an isomorphism. This is proved in ShortExactFiveLemma.Definition ShortExactObs1 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowObs A.
Show proof.
use make_FiveRowObs.
- exact (to_Zero A).
- exact (Ob1 SSE1).
- exact (Ob2 SSE1).
- exact (Ob3 SSE1).
- exact (to_Zero A).
- exact (to_Zero A).
- exact (Ob1 SSE1).
- exact (Ob2 SSE1).
- exact (Ob3 SSE1).
- exact (to_Zero A).
Definition ShortExactDiffs1 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowDiffs A (ShortExactObs1 Mor).
Show proof.
use make_FiveRowDiffs.
- exact (ZeroArrow (to_Zero A) _ _).
- exact (Mor1 SSE1).
- exact (Mor2 SSE1).
- exact (ZeroArrow (to_Zero A) _ _).
- exact (ZeroArrow (to_Zero A) _ _).
- exact (Mor1 SSE1).
- exact (Mor2 SSE1).
- exact (ZeroArrow (to_Zero A) _ _).
Lemma ShortExactDiffsEq1 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowDiffsEq A _ (ShortExactDiffs1 Mor).
Show proof.
use make_FiveRowDiffsEq.
- cbn. apply ZeroArrow_comp_left.
- cbn. use (ShortShortExactData_Eq (to_Zero A) SSE1).
- cbn. apply ZeroArrow_comp_right.
- cbn. apply ZeroArrow_comp_left.
- cbn. use (ShortShortExactData_Eq (to_Zero A) SSE1).
- cbn. apply ZeroArrow_comp_right.
Lemma ShortExactExacts1 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowExacts A _ _ (ShortExactDiffsEq1 Mor).
Show proof.
use make_FiveRowExacts.
- cbn. use isExactisMonic. exact (ShortExactSequences.isMonic SSE1).
- unfold isExact. exact (ShortShortExact_isKernel SSE1).
- cbn. use isExactisEpi. exact (ShortExactSequences.isEpi SSE1).
- cbn. use isExactisMonic. exact (ShortExactSequences.isMonic SSE1).
- unfold isExact. exact (ShortShortExact_isKernel SSE1).
- cbn. use isExactisEpi. exact (ShortExactSequences.isEpi SSE1).
Definition ShortExactRow1 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRow A.
Show proof.
use make_FiveRow.
- exact (ShortExactObs1 Mor).
- exact (ShortExactDiffs1 Mor).
- exact (ShortExactDiffsEq1 Mor).
- exact (ShortExactExacts1 Mor).
- exact (ShortExactObs1 Mor).
- exact (ShortExactDiffs1 Mor).
- exact (ShortExactDiffsEq1 Mor).
- exact (ShortExactExacts1 Mor).
Definition ShortExactObs2 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowObs A.
Show proof.
use make_FiveRowObs.
- exact (to_Zero A).
- exact (Ob1 SSE2).
- exact (Ob2 SSE2).
- exact (Ob3 SSE2).
- exact (to_Zero A).
- exact (to_Zero A).
- exact (Ob1 SSE2).
- exact (Ob2 SSE2).
- exact (Ob3 SSE2).
- exact (to_Zero A).
Definition ShortExactDiffs2 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowDiffs A (ShortExactObs2 Mor).
Show proof.
use make_FiveRowDiffs.
- exact (ZeroArrow (to_Zero A) _ _).
- exact (Mor1 SSE2).
- exact (Mor2 SSE2).
- exact (ZeroArrow (to_Zero A) _ _).
- exact (ZeroArrow (to_Zero A) _ _).
- exact (Mor1 SSE2).
- exact (Mor2 SSE2).
- exact (ZeroArrow (to_Zero A) _ _).
Lemma ShortExactDiffsEq2 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowDiffsEq A _ (ShortExactDiffs2 Mor).
Show proof.
use make_FiveRowDiffsEq.
- cbn. apply ZeroArrow_comp_left.
- cbn. use (ShortShortExactData_Eq (to_Zero A) SSE2).
- cbn. apply ZeroArrow_comp_right.
- cbn. apply ZeroArrow_comp_left.
- cbn. use (ShortShortExactData_Eq (to_Zero A) SSE2).
- cbn. apply ZeroArrow_comp_right.
Lemma ShortExactExacts2 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowExacts A _ _ (ShortExactDiffsEq2 Mor).
Show proof.
use make_FiveRowExacts.
- cbn. use isExactisMonic. exact (ShortExactSequences.isMonic SSE2).
- unfold isExact. exact (ShortShortExact_isKernel SSE2).
- cbn. use isExactisEpi. exact (ShortExactSequences.isEpi SSE2).
- cbn. use isExactisMonic. exact (ShortExactSequences.isMonic SSE2).
- unfold isExact. exact (ShortShortExact_isKernel SSE2).
- cbn. use isExactisEpi. exact (ShortExactSequences.isEpi SSE2).
Definition ShortExactRow2 {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRow A.
Show proof.
use make_FiveRow.
- exact (ShortExactObs2 Mor).
- exact (ShortExactDiffs2 Mor).
- exact (ShortExactDiffsEq2 Mor).
- exact (ShortExactExacts2 Mor).
- exact (ShortExactObs2 Mor).
- exact (ShortExactDiffs2 Mor).
- exact (ShortExactDiffsEq2 Mor).
- exact (ShortExactExacts2 Mor).
Definition ShortExactMors {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowMors A (ShortExactRow1 Mor) (ShortExactRow2 Mor).
Show proof.
use make_FiveRowMors.
- exact (identity _).
- exact (MPMor1 Mor).
- exact (MPMor2 Mor).
- exact (MPMor3 Mor).
- exact (identity _).
- exact (identity _).
- exact (MPMor1 Mor).
- exact (MPMor2 Mor).
- exact (MPMor3 Mor).
- exact (identity _).
Lemma ShortExactMorComm {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowMorsComm A _ _ (ShortExactMors Mor).
Show proof.
use make_FiveRowMorsComm.
- cbn. rewrite ZeroArrow_comp_left. rewrite id_left. apply idpath.
- cbn. exact (! (MPComm1 Mor)).
- cbn. exact (! (MPComm2 Mor)).
- cbn. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_right. apply idpath.
- cbn. rewrite ZeroArrow_comp_left. rewrite id_left. apply idpath.
- cbn. exact (! (MPComm1 Mor)).
- cbn. exact (! (MPComm2 Mor)).
- cbn. rewrite ZeroArrow_comp_left. rewrite ZeroArrow_comp_right. apply idpath.
Definition ShortExactMor {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2) :
@FiveRowMorphism A (ShortExactRow1 Mor) (ShortExactRow2 Mor).
Show proof.
Lemma ShortExactFiveLemma {SSE1 SSE2 : ShortExact A} (Mor : MPMor SSE1 SSE2)
(H2 : is_z_isomorphism (MPMor1 Mor)) (H4 : is_z_isomorphism (MPMor3 Mor)) :
is_z_isomorphism (MPMor2 Mor).
Show proof.
set (FR1 := ShortExactRow1 Mor).
set (FR2 := ShortExactRow2 Mor).
set (FM := ShortExactMor Mor).
use (FiveLemma FM).
- exact (is_z_isomorphism_identity _).
- exact H2.
- exact H4.
- exact (is_z_isomorphism_identity _).
set (FR2 := ShortExactRow2 Mor).
set (FM := ShortExactMor Mor).
use (FiveLemma FM).
- exact (is_z_isomorphism_identity _).
- exact H2.
- exact H4.
- exact (is_z_isomorphism_identity _).
End short_exact_five_lemma.