Documentation

DerivedAlgGeo.CategoryTheory.Abelian.Stability.Uniqueness.MonoDescent

Descent of HN filtrations along a monomorphism #

This file owns the normalization lemmas of the owner-native uniqueness argument: phase and semistability are invariant under propositional rewriting of a successive quotient, a subobject of the domain of a monomorphism is carried isomorphically to its image, and an HN filtration of a subobject can be extended by the mono. It closes with the semistable base case that produces an HN filtration whose last phase is prescribed.

source
theorem CategoryTheory.Triangulated.StabilityFunction.phase_cokernel_ofLE_congr {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} {A₁ A₂ B₁ B₂ : Subobject E} (hA : A₁ = A₂) (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} :
Z.phase (Limits.cokernel (A₁.ofLE B₁ h₁)) = Z.phase (Limits.cokernel (A₂.ofLE B₂ h₂))

Phase equality after propositionally rewriting both subobjects in a successive quotient.

source
theorem CategoryTheory.Triangulated.StabilityFunction.isSemistable_cokernel_ofLE_congr {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} {A₁ A₂ B₁ B₂ : Subobject E} (hA : A₁ = A₂) (hB : B₁ = B₂) {h₁ : A₁ ≤ B₁} {h₂ : A₂ ≤ B₂} (hs : Z.IsSemistable (Limits.cokernel (A₂.ofLE B₂ h₂))) :
Z.IsSemistable (Limits.cokernel (A₁.ofLE B₁ h₁))

Semistability is preserved after propositionally rewriting both subobjects in a successive quotient.

source
theorem CategoryTheory.Triangulated.StabilityFunction.Subobject.map_eq_mk_mono {A : Type u} [Category.{v, u} A] {X Y : A} (f : X ⟶ Y) [Mono f] (S : Subobject X) :
(Subobject.map f).obj S = Subobject.mk (CategoryStruct.comp S.arrow f)

Mapping a subobject along a monomorphism agrees with the subobject represented by the composite arrow.

source
noncomputable def CategoryTheory.Triangulated.StabilityFunction.Subobject.mapMonoIso {A : Type u} [Category.{v, u} A] {X Y : A} (f : X ⟶ Y) [Mono f] (S : Subobject X) :
Subobject.underlying.obj ((Subobject.map f).obj S) ≅ Subobject.underlying.obj S

A subobject and its image under a monomorphism have canonically isomorphic underlying objects.

Equations
Instances For
    source
    theorem CategoryTheory.Triangulated.StabilityFunction.Subobject.ofLE_map_comp_mapMonoIso_hom {A : Type u} [Category.{v, u} A] {X Y : A} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) :
    CategoryStruct.comp (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯) (mapMonoIso f T).hom = CategoryStruct.comp (mapMonoIso f S).hom (S.ofLE T h)
    source
    noncomputable def CategoryTheory.Triangulated.StabilityFunction.Subobject.cokernelMapMonoIso {A : Type u} [Category.{v, u} A] [Abelian A] {X Y : A} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) :
    Limits.cokernel (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯) ≅ Limits.cokernel (S.ofLE T h)

    Successive quotients are unchanged when a subobject chain is mapped along a monomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Triangulated.StabilityFunction.phase_cokernel_mapMono_eq {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {X Y : A} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) :
      Z.phase (Limits.cokernel (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯)) = Z.phase (Limits.cokernel (S.ofLE T h))
      source
      theorem CategoryTheory.Triangulated.StabilityFunction.isSemistable_cokernel_mapMono_iff {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {X Y : A} (f : X ⟶ Y) [Mono f] {S T : Subobject X} (h : S ≤ T) :
      Z.IsSemistable (Limits.cokernel (((Subobject.map f).obj S).ofLE ((Subobject.map f).obj T) ⋯)) ↔ Z.IsSemistable (Limits.cokernel (S.ofLE T h))
      source
      theorem CategoryTheory.Triangulated.StabilityFunction.append_hn_filtration_of_mono {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {X Y B : A} (i : X ⟶ Y) [Mono i] (F : AbelianHNFiltration Z X) (eB : Limits.cokernel i ≅ B) (hB : Z.IsSemistable B) (hlast : Z.phase B < F.phase ⟨F.n - 1, ⋯⟩) :
      ∃ (G : AbelianHNFiltration Z Y), G.phase ⟨G.n - 1, ⋯⟩ = Z.phase B

      Append a lower-phase semistable quotient to an owner abelian HN filtration along a monomorphism.

      source
      theorem CategoryTheory.Triangulated.StabilityFunction.exists_hn_with_last_phase_of_semistable {A : Type u} [Category.{v, u} A] [Abelian A] (Z : StabilityFunction A) {E : A} (hE : Z.IsSemistable E) :
      ∃ (F : AbelianHNFiltration Z E), F.phase ⟨F.n - 1, ⋯⟩ = Z.phase E

      The one-factor owner HN filtration of a semistable abelian object.