The subobject lattice of an HN filtration

This file owns the lattice bookkeeping of the uniqueness argument: an HN filtration has one factor exactly when its object is semistable, pullback along a cokernel projection is compatible with the chain and with charge, and the canonical comparison cokernelPullbackIso identifies the cokernel of a pullback with the pullback of a cokernel.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.n_eq_one_of_semistable {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (hE : Z.IsSemistable E) : F.n = 1

A semistable object can only have a one-factor HN filtration.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.isSemistable_of_n_eq_one {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (hn : F.n = 1) : Z.IsSemistable E

A one-factor HN filtration identifies its ambient object as semistable.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.n_eq_one_iff_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) : F.n = 1 ↔ Z.IsSemistable E

A one-factor HN filtration is equivalent to semistability of its ambient object.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.two_le_n_of_not_isSemistable {A : Type u} [Category.{v, u} A] [Abelian A] {Z : StabilityFunction A} {E : A} (F : AbelianHNFiltration Z E) (hE : ¬Z.IsSemistable E) : 2 ≤ F.n

A non-semistable object has at least two HN factors.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.le_of_arrow_comp_cokernel_zero {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} {B M : Subobject E} (h : CategoryStruct.comp B.arrow (Limits.cokernel.π M.arrow) = 0) : B ≤ M

If a subobject maps trivially to the quotient by another subobject, it is contained in that subobject.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.le_of_ofLE_comp_cokernel_zero {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} {B M S : Subobject E} (hBS : B ≤ S) (hMS : M ≤ S) (h : CategoryStruct.comp (B.ofLE S hBS) (Limits.cokernel.π (M.ofLE S hMS)) = 0) : B ≤ M

The relative form of le_of_arrow_comp_cokernel_zero: a subobject of S that maps trivially to the quotient S / M is contained in M.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.pullback_cokernel_bot_eq {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (M : Subobject E) : (Subobject.pullback (Limits.cokernel.π M.arrow)).obj ⊥ = M

Pulling bottom back along the quotient by a subobject recovers the subobject.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.card_subobject_cokernel_lt {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} {M : Subobject E} (hM : M ≠ ⊥) [Finite (Subobject E)] : Nat.card (Subobject (Limits.cokernel M.arrow)) < Nat.card (Subobject E)

Quotienting by a nonzero subobject strictly decreases a finite subobject lattice.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.le_pullback_cokernel {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (M : Subobject E) (B : Subobject (Limits.cokernel M.arrow)) : M ≤ (Subobject.pullback (Limits.cokernel.π M.arrow)).obj B

Every subobject of a quotient pulls back to a subobject containing the kernel of the quotient map.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.ofLE_pullbackπ_cokernel_eq_zero {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (M : Subobject E) (B : Subobject (Limits.cokernel M.arrow)) : CategoryStruct.comp (M.ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B) ⋯) (Subobject.pullbackπ (Limits.cokernel.π M.arrow) B) = 0

The kernel inclusion followed by the restricted quotient map is zero.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.shortExact_ofLE_pullbackπ_cokernel {A : Type u} [Category.{v, u} A] [Abelian A] {E : A} (M : Subobject E) (B : Subobject (Limits.cokernel M.arrow)) : { X₁ := Subobject.underlying.obj M, X₂ := Subobject.underlying.obj ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B), X₃ := Subobject.underlying.obj B, f := M.ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B) ⋯, g := Subobject.pullbackπ (Limits.cokernel.π M.arrow) B, zero := ⋯ }.ShortExact

Pulling a subobject of a quotient back gives a canonical short exact sequence with the quotient kernel.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.charge_pullback_eq_add {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} (M : Subobject E) (B : Subobject (Limits.cokernel M.arrow)) : Z.charge (Subobject.underlying.obj ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B)) = Z.charge (Subobject.underlying.obj M) + Z.charge (Subobject.underlying.obj B)

The charge of a pulled-back quotient subobject is the sum of the kernel charge and the subobject charge.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.pullback_imageSubobject_eq {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} {M S : Subobject E} (hMS : M ≤ S) : (Subobject.pullback (Limits.cokernel.π M.arrow)).obj (Limits.imageSubobject (CategoryStruct.comp S.arrow (Limits.cokernel.π M.arrow))) = S

Pulling the image of a subobject containing the quotient kernel back along the quotient projection recovers the original subobject.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.charge_cokernel_pullback_eq {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} (M : Subobject E) {B₁ B₂ : Subobject (Limits.cokernel M.arrow)} (h : B₁ ≤ B₂) : Z.charge (Limits.cokernel (((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₁).ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₂) ⋯)) = Z.charge (Limits.cokernel (B₁.ofLE B₂ h))

Consecutive pulled-back quotient subobjects have the same charge as the corresponding quotient factor.

theorem CategoryTheory.Triangulated.AbelianHNFiltration.phase_cokernel_pullback_eq {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} (M : Subobject E) {B₁ B₂ : Subobject (Limits.cokernel M.arrow)} (h : B₁ ≤ B₂) : Z.phase (Limits.cokernel (((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₁).ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₂) ⋯)) = Z.phase (Limits.cokernel (B₁.ofLE B₂ h))

Consecutive pulled-back quotient subobjects have the same phase as the corresponding quotient factor.

noncomputable def CategoryTheory.Triangulated.AbelianHNFiltration.cokernelPullbackIso {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} (M : Subobject E) {B₁ B₂ : Subobject (Limits.cokernel M.arrow)} (h : B₁ < B₂) : Limits.cokernel (((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₁).ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B₂) ⋯) ≅ Limits.cokernel (B₁.ofLE B₂ ⋯)

Consecutive pulled-back quotient factors are canonically isomorphic.

Equations

• One or more equations did not get rendered due to their size.