Exact sequences with four terms #
The main definition in this file is ComposableArrows.Exact.cokerIsoKer:
given an exact sequence S (involving at least four objects),
this is the isomorphism from the cokernel of S.map' k (k + 1)
to the kernel of S.map' (k + 2) (k + 3). This is intended
to be used for exact sequences in abelian categories, but the
construction works for preadditive balanced categories.
def
CategoryTheory.ComposableArrows.IsComplex.cokerToKer'
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
If S is a complex, this is the morphism from a cokernel of S.map' k (k + 1)
to a kernel of S.map' (k + 2) (k + 3).
Equations
- hS.cokerToKer' k hk cc kf hcc hkf = hcc.desc (CategoryTheory.Limits.CokernelCofork.ofπ (hkf.lift (CategoryTheory.Limits.KernelFork.ofι (S.map' (k + 1) (k + 1 + 1) ⋯ ⋯) ⋯)) ⋯)
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
CategoryStruct.comp (Limits.Cofork.π cc) (CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (Limits.Fork.ι kf)) = S.map' (k + 1) (k + 2) ⋯ ⋯
@[simp]
theorem
CategoryTheory.ComposableArrows.IsComplex.cokerToKer'_fac_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
{Z : C}
(h : S.obj ⟨k + 2, ⋯⟩ ⟶ Z)
:
CategoryStruct.comp (Limits.Cofork.π cc)
(CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (CategoryStruct.comp (Limits.Fork.ι kf) h)) = CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
noncomputable def
CategoryTheory.ComposableArrows.IsComplex.cokerToKer
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n := by lia)
[Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
[Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)]
:
If S is a complex, this is the morphism from the cokernel of S.map' k (k + 1)
to the kernel of S.map' (k + 2) (k + 3).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n := by lia)
[Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
[Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)]
:
CategoryStruct.comp (Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
(CategoryStruct.comp (hS.cokerToKer k hk) (Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯))) = S.map' (k + 1) (k + 2) ⋯ ⋯
@[simp]
theorem
CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n := by lia)
[Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
[Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)]
{Z : C}
(h : S.obj ⟨k + 2, ⋯⟩ ⟶ Z)
:
CategoryStruct.comp (Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
(CategoryStruct.comp (hS.cokerToKer k hk) (CategoryStruct.comp (Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯)) h)) = CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
noncomputable def
CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n := by lia)
[(S.sc hS k ⋯).HasRightHomology]
[(S.sc hS (k + 1) ⋯).HasLeftHomology]
:
If S is a complex, this is the morphism from the opcycles of S in
degree k + 1 to the cycles of S in degree k + 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n := by lia)
[(S.sc hS k ⋯).HasRightHomology]
[(S.sc hS (k + 1) ⋯).HasLeftHomology]
:
CategoryStruct.comp (S.sc hS k ⋯).pOpcycles
(CategoryStruct.comp (hS.opcyclesToCycles k ⋯) (S.sc hS (k + 1) ⋯).iCycles) = S.map' (k + 1) (k + 2) ⋯ ⋯
@[simp]
theorem
CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[Limits.HasZeroMorphisms C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n := by lia)
[(S.sc hS k ⋯).HasRightHomology]
[(S.sc hS (k + 1) ⋯).HasLeftHomology]
{Z : C}
(h : S.obj ⟨k + 1 + 1, ⋯⟩ ⟶ Z)
:
CategoryStruct.comp (S.sc hS k ⋯).pOpcycles
(CategoryStruct.comp (hS.opcyclesToCycles k ⋯) (CategoryStruct.comp (S.sc hS (k + 1) ⋯).iCycles h)) = CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
theorem
CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer'
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
(hS' : (S.sc hS (k + 1) ⋯).Exact)
:
Epi (hS.cokerToKer' k hk cc kf hcc hkf)
theorem
CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer'
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.IsComplex)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
(hS' : (S.sc hS k ⋯).Exact)
:
Mono (hS.cokerToKer' k hk cc kf hcc hkf)
@[reducible, inline]
abbrev
CategoryTheory.ComposableArrows.Exact.cokerToKer'
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
If S is an exact sequence, this is the morphism from a cokernel
of S.map' k (k + 1) to a kernel of S.map' (k + 2) (k + 3).
Equations
- hS.cokerToKer' k hk cc kf hcc hkf = ⋯.cokerToKer' k hk cc kf hcc hkf
Instances For
instance
CategoryTheory.ComposableArrows.Exact.isIso_cokerToKer'
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
IsIso (hS.cokerToKer' k hk cc kf hcc hkf)
noncomputable def
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
If S is an exact sequence, this is the isomorphism from a cokernel
of S.map' k (k + 1) to a kernel of S.map' (k + 2) (k + 3).
Equations
- hS.cokerIsoKer' k hk cc kf hcc hkf = CategoryTheory.asIso (hS.cokerToKer' k hk cc kf hcc hkf)
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) (hS.cokerIsoKer' k hk cc kf hcc hkf).inv = CategoryStruct.id cc.pt
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_hom_inv_id_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
{Z : C}
(h : cc.pt ⟶ Z)
:
CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf)
(CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv h) = h
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
:
CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv (hS.cokerToKer' k hk cc kf hcc hkf) = CategoryStruct.id kf.pt
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.cokerIsoKer'_inv_hom_id_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n)
(cc : Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
(kf : Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯))
(hcc : Limits.IsColimit cc)
(hkf : Limits.IsLimit kf)
{Z : C}
(h : kf.pt ⟶ Z)
:
CategoryStruct.comp (hS.cokerIsoKer' k hk cc kf hcc hkf).inv
(CategoryStruct.comp (hS.cokerToKer' k hk cc kf hcc hkf) h) = h
noncomputable def
CategoryTheory.ComposableArrows.Exact.cokerIsoKer
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n := by lia)
[Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
[Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)]
:
If S is an exact sequence, this is the isomorphism from the cokernel
of S.map' k (k + 1) to the kernel of S.map' (k + 2) (k + 3).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n := by lia)
[Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
[Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)]
:
CategoryStruct.comp (Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
(CategoryStruct.comp (hS.cokerIsoKer k ⋯).hom (Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯))) = S.map' (k + 1) (k + 2) ⋯ ⋯
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n := by lia)
[Limits.HasCokernel (S.map' k (k + 1) ⋯ ⋯)]
[Limits.HasKernel (S.map' (k + 2) (k + 3) ⋯ ⋯)]
{Z : C}
(h : S.obj ⟨k + 2, ⋯⟩ ⟶ Z)
:
CategoryStruct.comp (Limits.cokernel.π (S.map' k (k + 1) ⋯ ⋯))
(CategoryStruct.comp (hS.cokerIsoKer k ⋯).hom
(CategoryStruct.comp (Limits.kernel.ι (S.map' (k + 2) (k + 3) ⋯ ⋯)) h)) = CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h
noncomputable def
CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n := by lia)
[h₁ : (hS.sc k ⋯).HasRightHomology]
[h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology]
:
If S is an exact sequence, this is the isomorphism from the opcycles of S in
degree k + 1 to the cycles of S in degree k + 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n := by lia)
[h₁ : (hS.sc k ⋯).HasRightHomology]
[h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology]
:
CategoryStruct.comp (hS.sc k ⋯).pOpcycles
(CategoryStruct.comp (hS.opcyclesIsoCycles k ⋯).hom (hS.sc (k + 1) ⋯).iCycles) = S.map' (k + 1) (k + 2) ⋯ ⋯
@[simp]
theorem
CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc
{C : Type u_1}
[Category.{u_2, u_1} C]
[Preadditive C]
[Balanced C]
{n : ℕ}
{S : ComposableArrows C (n + 3)}
(hS : S.Exact)
(k : ℕ)
(hk : k ≤ n := by lia)
[h₁ : (hS.sc k ⋯).HasRightHomology]
[h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology]
{Z : C}
(h : S.obj ⟨k + 1 + 1, ⋯⟩ ⟶ Z)
:
CategoryStruct.comp (hS.sc k ⋯).pOpcycles
(CategoryStruct.comp (hS.opcyclesIsoCycles k ⋯).hom (CategoryStruct.comp (hS.sc (k + 1) ⋯).iCycles h)) = CategoryStruct.comp (S.map' (k + 1) (k + 2) ⋯ ⋯) h