Finite filtrations in an abelian category

This file records the common categorical root of finite filtrations. FiniteExactTower owns the successive short exact sequences; a FiniteFiltration M extends that parent with a proof that its bottom is zero and a chosen identification of its top with M.

When a graded piece is itself filtered, FiniteFiltration.pullbackTower pulls its stages back along the coarse quotient projection. The endpoint comparison isomorphisms identify the new tower with the adjacent coarse stages, providing the categorical splice data used by almost-disconnected composition. FiniteExactTower.replaceSteps assembles a family of such replacement towers, and FiniteFiltration.refineAll supplies the abelian quotient-pullback specialization.

Keeping this root independent of schemes prevents geometric filtrations (for example, the almost-disconnected filtrations of arXiv:2607.28411, Appendix B) from growing their own incompatible tower type.

structure CategoryTheory.FiniteExactTower (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] : Type (max u v)

A finite tower of successive short exact extensions.

This is the endpoint-free categorical parent of FiniteFiltration. It is useful when a filtration of a quotient is pulled back to a tower beginning at the kernel: that intermediate tower does not itself begin at zero, so it must not be encoded as a second filtration type or by putting a false endpoint condition into a structure field.

• length : ℕ

  The number of graded pieces.

• object : Fin (self.length + 1) → C

  The objects T₀, ..., Tₙ in the tower.

• inclusion (i : Fin self.length) : self.object i.castSucc ⟶ self.object i.succ

  The inclusion Tᵢ ⟶ Tᵢ₊₁.

• graded : Fin self.length → C

  The ith graded piece Tᵢ₊₁/Tᵢ.

• projection (i : Fin self.length) : self.object i.succ ⟶ self.graded i

  The quotient projection Tᵢ₊₁ ⟶ Tᵢ₊₁/Tᵢ.

• zero (i : Fin self.length) : CategoryStruct.comp (self.inclusion i) (self.projection i) = 0

  Consecutive maps compose to zero.

• shortExact (i : Fin self.length) : { X₁ := self.object i.castSucc, X₂ := self.object i.succ, X₃ := self.graded i, f := self.inclusion i, g := self.projection i, zero := ⋯ }.ShortExact

  Each step realizes its named graded piece as the quotient.

structure CategoryTheory.FiniteFiltration (C : Type u) [Category.{v, u} C] [Limits.HasZeroMorphisms C] (M : C) extends CategoryTheory.FiniteExactTower C : Type (max u v)

A finite filtration of an object by successive short exact sequences.

object i.castSucc ⟶ object i.succ ⟶ graded i is the ith short exact sequence. The endpoint data express F₀ = 0 and Fₙ = M without making either equality definitional.

• length : ℕ
• object : Fin (self.length + 1) → C
• inclusion (i : Fin self.length) : self.object i.castSucc ⟶ self.object i.succ
• graded : Fin self.length → C
• projection (i : Fin self.length) : self.object i.succ ⟶ self.graded i
• zero (i : Fin self.length) : CategoryStruct.comp (self.inclusion i) (self.projection i) = 0
• shortExact (i : Fin self.length) : { X₁ := self.object i.castSucc, X₂ := self.object i.succ, X₃ := self.graded i, f := self.inclusion i, g := self.projection i, zero := ⋯ }.ShortExact
• initialIsZero : Limits.IsZero (self.object 0)

  The bottom term is zero.

• terminalIso : self.object (Fin.last self.length) ≅ M

  The top term is the filtered object.

def CategoryTheory.FiniteExactTower.step {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (i : Fin T.length) : ShortComplex C

The short complex presenting the ith successive quotient.

Equations

• T.step i = { X₁ := T.object i.castSucc, X₂ := T.object i.succ, X₃ := T.graded i, f := T.inclusion i, g := T.projection i, zero := ⋯ }

theorem CategoryTheory.FiniteExactTower.step_shortExact {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (i : Fin T.length) : (T.step i).ShortExact

noncomputable def CategoryTheory.FiniteExactTower.diagram {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) : ComposableArrows C T.length

The composable-arrow diagram canonically generated by the successive inclusions.

Equations

• T.diagram = CategoryTheory.ComposableArrows.mkOfObjOfMapSucc T.object T.inclusion

@[simp]

theorem CategoryTheory.FiniteExactTower.diagram_obj {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (i : Fin (T.length + 1)) : T.diagram.obj i = T.object i

theorem CategoryTheory.FiniteExactTower.diagram_map_succ {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (i : Fin T.length) : T.diagram.map (homOfLE ⋯) = T.inclusion i

noncomputable def CategoryTheory.FiniteExactTower.toTop {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (i : Fin (T.length + 1)) : T.object i ⟶ T.object (Fin.last T.length)

The canonical composite from any stage to the top of the tower.

Equations

• T.toTop i = T.diagram.map (CategoryTheory.homOfLE ⋯)

@[simp]

theorem CategoryTheory.FiniteExactTower.toTop_last {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) : T.toTop (Fin.last T.length) = CategoryStruct.id (T.object (Fin.last T.length))

theorem CategoryTheory.FiniteExactTower.inclusion_toTop {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (i : Fin T.length) : CategoryStruct.comp (T.inclusion i) (T.toTop i.succ) = T.toTop i.castSucc

def CategoryTheory.FiniteExactTower.gradedObjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) : List C

The ordered list of successive quotients in an exact tower.

Equations

• T.gradedObjects = List.ofFn T.graded

def CategoryTheory.FiniteExactTower.take {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : FiniteExactTower C

The initial segment ending at a chosen stage of an exact tower.

Equations

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

@[simp]

theorem CategoryTheory.FiniteExactTower.take_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.take k).length = ↑k

@[simp]

theorem CategoryTheory.FiniteExactTower.take_gradedObjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.take k).gradedObjects = List.take (↑k) T.gradedObjects

noncomputable def CategoryTheory.FiniteExactTower.takeInitialIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.take k).object 0 ≅ T.object 0

The start of an initial segment agrees with the start of the original tower.

Equations

• T.takeInitialIso k = CategoryTheory.eqToIso ⋯

noncomputable def CategoryTheory.FiniteExactTower.takeTerminalIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.take k).object (Fin.last (T.take k).length) ≅ T.object k

The end of an initial segment is its selected original stage.

Equations

• T.takeTerminalIso k = CategoryTheory.eqToIso ⋯

def CategoryTheory.FiniteExactTower.drop {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : FiniteExactTower C

The terminal segment beginning at a chosen stage of an exact tower.

Equations

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

@[simp]

theorem CategoryTheory.FiniteExactTower.drop_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.drop k).length = T.length - ↑k

@[simp]

theorem CategoryTheory.FiniteExactTower.drop_gradedObjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.drop k).gradedObjects = List.drop (↑k) T.gradedObjects

noncomputable def CategoryTheory.FiniteExactTower.dropInitialIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.drop k).object 0 ≅ T.object k

The start of a terminal segment is its selected original stage.

Equations

• T.dropInitialIso k = CategoryTheory.eqToIso ⋯

noncomputable def CategoryTheory.FiniteExactTower.dropTerminalIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (k : Fin (T.length + 1)) : (T.drop k).object (Fin.last (T.drop k).length) ≅ T.object (Fin.last T.length)

The end of a terminal segment agrees with the end of the original tower.

Equations

• T.dropTerminalIso k = CategoryTheory.eqToIso ⋯

def CategoryTheory.FiniteExactTower.prepend {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) {X G : C} (f : X ⟶ T.object 0) (g : T.object 0 ⟶ G) (zero : CategoryStruct.comp f g = 0) (shortExact : { X₁ := X, X₂ := T.object 0, X₃ := G, f := f, g := g, zero := zero }.ShortExact) : FiniteExactTower C

Prepend one short exact step to an exact tower.

This is the primitive from which endpoint-compatible towers are concatenated. Adding at the left edge keeps the Fin embeddings definitional, avoiding transports between the two distinct right-edge embeddings i.castSucc.succ and i.succ.castSucc.

Equations

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

@[simp]

theorem CategoryTheory.FiniteExactTower.prepend_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) {X G : C} (f : X ⟶ T.object 0) (g : T.object 0 ⟶ G) (zero : CategoryStruct.comp f g = 0) (shortExact : { X₁ := X, X₂ := T.object 0, X₃ := G, f := f, g := g, zero := zero }.ShortExact) : (T.prepend f g zero shortExact).length = T.length + 1

noncomputable def CategoryTheory.FiniteExactTower.append {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T U : FiniteExactTower C) (seam : T.object (Fin.last T.length) ≅ U.object 0) : FiniteExactTower C

Concatenate two exact towers along an isomorphism from the left endpoint to the right start.

The result contains the graded pieces of T, followed by those of U. The seam is an isomorphism rather than an equality because pulled-back quotient filtrations meet their adjacent coarse stages canonically only up to isomorphism.

Equations

• T.append U seam = CategoryTheory.FiniteExactTower.AppendData.tower✝ (CategoryTheory.FiniteExactTower.appendData✝ T U seam)

@[simp]

theorem CategoryTheory.FiniteExactTower.append_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T U : FiniteExactTower C) (seam : T.object (Fin.last T.length) ≅ U.object 0) : (T.append U seam).length = T.length + U.length

@[simp]

theorem CategoryTheory.FiniteExactTower.append_gradedObjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T U : FiniteExactTower C) (seam : T.object (Fin.last T.length) ≅ U.object 0) : (T.append U seam).gradedObjects = T.gradedObjects ++ U.gradedObjects

noncomputable def CategoryTheory.FiniteExactTower.appendInitialIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T U : FiniteExactTower C) (seam : T.object (Fin.last T.length) ≅ U.object 0) : T.object 0 ≅ (T.append U seam).object 0

The start of a concatenation is canonically the start of its left tower.

Equations

• T.appendInitialIso U seam = CategoryTheory.FiniteExactTower.AppendData.initialIso✝ (CategoryTheory.FiniteExactTower.appendData✝ T U seam)

noncomputable def CategoryTheory.FiniteExactTower.appendTerminalIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T U : FiniteExactTower C) (seam : T.object (Fin.last T.length) ≅ U.object 0) : (T.append U seam).object (Fin.last (T.append U seam).length) ≅ U.object (Fin.last U.length)

The end of a concatenation is canonically the end of its right tower.

Equations

• T.appendTerminalIso U seam = CategoryTheory.FiniteExactTower.AppendData.terminalIso✝ (CategoryTheory.FiniteExactTower.appendData✝ T U seam)

noncomputable def CategoryTheory.FiniteExactTower.replaceSteps {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (R : Fin T.length → FiniteExactTower C) (start : (i : Fin T.length) → (R i).object 0 ≅ T.object i.castSucc) (finish : (i : Fin T.length) → (R i).object (Fin.last (R i).length) ≅ T.object i.succ) : FiniteExactTower C

Simultaneously replace every step of an exact tower by an endpoint-compatible exact tower.

This is the many-step parent of FiniteFiltration.refineStep. It is deliberately owned by FiniteExactTower: geometric consumers provide replacement towers, while their concatenation, ordering, and endpoint bookkeeping remain common categorical infrastructure.

Equations

• T.replaceSteps R start finish = CategoryTheory.FiniteExactTower.ReplaceStepsData.tower✝ (CategoryTheory.FiniteExactTower.replaceStepsData✝ T R start finish)

@[simp]

theorem CategoryTheory.FiniteExactTower.replaceSteps_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (R : Fin T.length → FiniteExactTower C) (start : (i : Fin T.length) → (R i).object 0 ≅ T.object i.castSucc) (finish : (i : Fin T.length) → (R i).object (Fin.last (R i).length) ≅ T.object i.succ) : (T.replaceSteps R start finish).length = (List.ofFn fun (i : Fin T.length) => (R i).length).sum

@[simp]

theorem CategoryTheory.FiniteExactTower.replaceSteps_gradedObjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (R : Fin T.length → FiniteExactTower C) (start : (i : Fin T.length) → (R i).object 0 ≅ T.object i.castSucc) (finish : (i : Fin T.length) → (R i).object (Fin.last (R i).length) ≅ T.object i.succ) : (T.replaceSteps R start finish).gradedObjects = (List.ofFn fun (i : Fin T.length) => (R i).gradedObjects).flatten

noncomputable def CategoryTheory.FiniteExactTower.replaceStepsInitialIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (R : Fin T.length → FiniteExactTower C) (start : (i : Fin T.length) → (R i).object 0 ≅ T.object i.castSucc) (finish : (i : Fin T.length) → (R i).object (Fin.last (R i).length) ≅ T.object i.succ) : T.object 0 ≅ (T.replaceSteps R start finish).object 0

The simultaneous replacement starts at the original tower's initial object.

Equations

• T.replaceStepsInitialIso R start finish = CategoryTheory.FiniteExactTower.ReplaceStepsData.initialIso✝ (CategoryTheory.FiniteExactTower.replaceStepsData✝ T R start finish)

noncomputable def CategoryTheory.FiniteExactTower.replaceStepsTerminalIso {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) (R : Fin T.length → FiniteExactTower C) (start : (i : Fin T.length) → (R i).object 0 ≅ T.object i.castSucc) (finish : (i : Fin T.length) → (R i).object (Fin.last (R i).length) ≅ T.object i.succ) : (T.replaceSteps R start finish).object (Fin.last (T.replaceSteps R start finish).length) ≅ T.object (Fin.last T.length)

The simultaneous replacement ends at the original tower's terminal object.

Equations

• T.replaceStepsTerminalIso R start finish = CategoryTheory.FiniteExactTower.ReplaceStepsData.terminalIso✝ (CategoryTheory.FiniteExactTower.replaceStepsData✝ T R start finish)

def CategoryTheory.FiniteExactTower.map {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (T : FiniteExactTower C) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : FiniteExactTower D

Apply an exact functor to an endpoint-free exact tower.

Equations

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

@[simp]

theorem CategoryTheory.FiniteExactTower.map_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (T : FiniteExactTower C) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : (T.map G).length = T.length

@[simp]

theorem CategoryTheory.FiniteExactTower.map_object {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (T : FiniteExactTower C) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (i : Fin ((T.map G).length + 1)) : (T.map G).object i = G.obj (T.object i)

@[simp]

theorem CategoryTheory.FiniteExactTower.map_graded {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (T : FiniteExactTower C) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (i : Fin (T.map G).length) : (T.map G).graded i = G.obj (T.graded i)

@[simp]

theorem CategoryTheory.FiniteExactTower.map_id {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (T : FiniteExactTower C) : T.map (Functor.id C) = T

@[simp]

theorem CategoryTheory.FiniteExactTower.map_comp {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (T : FiniteExactTower C) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] {E : Type u_1} [Category.{u_2, u_1} E] [Limits.HasZeroMorphisms E] (H : Functor D E) [H.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits H] [Limits.PreservesFiniteColimits H] : T.map (G.comp H) = (T.map G).map H

def CategoryTheory.FiniteFiltration.step {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) : ShortComplex C

The short complex presenting the ith successive quotient.

Equations

• F.step i = F.step i

theorem CategoryTheory.FiniteFiltration.step_shortExact {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) : (F.step i).ShortExact

instance CategoryTheory.FiniteFiltration.inclusion_mono {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) : Mono (F.inclusion i)

instance CategoryTheory.FiniteFiltration.projection_epi {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) : Epi (F.projection i)

noncomputable def CategoryTheory.FiniteFiltration.diagram {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) : ComposableArrows C F.length

The composable-arrow diagram underlying a finite filtration.

Equations

• F.diagram = F.diagram

noncomputable def CategoryTheory.FiniteFiltration.toObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin (F.length + 1)) : F.object i ⟶ M

The canonical map from a filtration stage to the filtered object.

Equations

• F.toObject i = CategoryTheory.CategoryStruct.comp (F.toTop i) F.terminalIso.hom

theorem CategoryTheory.FiniteFiltration.inclusion_toObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) : CategoryStruct.comp (F.inclusion i) (F.toObject i.succ) = F.toObject i.castSucc

@[simp]

theorem CategoryTheory.FiniteFiltration.toObject_zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) : F.toObject 0 = 0

def CategoryTheory.FiniteFiltration.map {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (F : FiniteFiltration C M) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : FiniteFiltration D (G.obj M)

Apply an exact functor to every term and every successive quotient of a finite filtration.

This is the common categorical operation used when a geometric filtration is pulled back by a flat morphism: the geometric leaf only has to identify its pullback functor and the images of the graded pieces. Exactness stays here, rather than being rebuilt in each almost-disconnected or stability-condition consumer.

Equations

• F.map G = { toFiniteExactTower := F.map G, initialIsZero := ⋯, terminalIso := G.mapIso F.terminalIso }

@[simp]

theorem CategoryTheory.FiniteFiltration.map_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (F : FiniteFiltration C M) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : (F.map G).length = F.length

@[simp]

theorem CategoryTheory.FiniteFiltration.map_object {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (F : FiniteFiltration C M) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (i : Fin ((F.map G).length + 1)) : (F.map G).object i = G.obj (F.object i)

@[simp]

theorem CategoryTheory.FiniteFiltration.map_graded {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (F : FiniteFiltration C M) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (i : Fin (F.map G).length) : (F.map G).graded i = G.obj (F.graded i)

@[simp]

theorem CategoryTheory.FiniteFiltration.map_id {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) : F.map (Functor.id C) = F

@[simp]

theorem CategoryTheory.FiniteFiltration.map_comp {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] (F : FiniteFiltration C M) (G : Functor C D) [G.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] {E : Type u_1} [Category.{u_2, u_1} E] [Limits.HasZeroMorphisms E] (H : Functor D E) [H.PreservesZeroMorphisms] [Limits.PreservesFiniteLimits H] [Limits.PreservesFiniteColimits H] : F.map (G.comp H) = (F.map G).map H

noncomputable def CategoryTheory.FiniteFiltration.replaceSteps {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (R : Fin F.length → FiniteExactTower C) (start : (i : Fin F.length) → (R i).object 0 ≅ F.object i.castSucc) (finish : (i : Fin F.length) → (R i).object (Fin.last (R i).length) ≅ F.object i.succ) : FiniteFiltration C M

Replace every step of a filtration by an endpoint-compatible exact tower.

The endpoint-free work is delegated to FiniteExactTower.replaceSteps; this specialization only transports the zero bottom and the chosen identification of the top with the filtered object.

Equations

• F.replaceSteps R start finish = { toFiniteExactTower := F.replaceSteps R start finish, initialIsZero := ⋯, terminalIso := F.replaceStepsTerminalIso R start finish ≪≫ F.terminalIso }

@[simp]

theorem CategoryTheory.FiniteFiltration.replaceSteps_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (R : Fin F.length → FiniteExactTower C) (start : (i : Fin F.length) → (R i).object 0 ≅ F.object i.castSucc) (finish : (i : Fin F.length) → (R i).object (Fin.last (R i).length) ≅ F.object i.succ) : (F.replaceSteps R start finish).length = (List.ofFn fun (i : Fin F.length) => (R i).length).sum

@[simp]

theorem CategoryTheory.FiniteFiltration.replaceSteps_gradedObjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (R : Fin F.length → FiniteExactTower C) (start : (i : Fin F.length) → (R i).object 0 ≅ F.object i.castSucc) (finish : (i : Fin F.length) → (R i).object (Fin.last (R i).length) ≅ F.object i.succ) : (F.replaceSteps R start finish).gradedObjects = (List.ofFn fun (i : Fin F.length) => (R i).gradedObjects).flatten

noncomputable def CategoryTheory.FiniteFiltration.spliceStep {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (T : FiniteExactTower C) (initialIso : T.object 0 ≅ F.object i.castSucc) (terminalIso : T.object (Fin.last T.length) ≅ F.object i.succ) : FiniteFiltration C M

Replace one step of a filtration by an endpoint-compatible exact tower.

The prefix and suffix come from the original filtration; the replacement tower supplies all steps between the adjacent coarse stages. This generic categorical operation is the common consumer of quotient pullback towers and does not depend on schemes or on the geometry of the graded pieces.

Equations

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

@[simp]

theorem CategoryTheory.FiniteFiltration.spliceStep_length {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (T : FiniteExactTower C) (initialIso : T.object 0 ≅ F.object i.castSucc) (terminalIso : T.object (Fin.last T.length) ≅ F.object i.succ) : (F.spliceStep i T initialIso terminalIso).length = F.length - 1 + T.length

@[simp]

theorem CategoryTheory.FiniteFiltration.spliceStep_gradedObjects {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (T : FiniteExactTower C) (initialIso : T.object 0 ≅ F.object i.castSucc) (terminalIso : T.object (Fin.last T.length) ≅ F.object i.succ) : (F.spliceStep i T initialIso terminalIso).gradedObjects = List.take (↑i) F.gradedObjects ++ T.gradedObjects ++ List.drop (↑i + 1) F.gradedObjects

@[reducible, inline]

noncomputable abbrev CategoryTheory.FiniteFiltration.pullbackObject {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin (F.length + 1)) : C

The stage obtained by pulling a filtration stage back along an epimorphism.

Equations

• CategoryTheory.FiniteFiltration.pullbackObject p F i = CategoryTheory.Limits.pullback p (F.toObject i)

noncomputable def CategoryTheory.FiniteFiltration.pullbackInclusion {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) : pullbackObject p F i.castSucc ⟶ pullbackObject p F i.succ

The inclusion between two consecutive pulled-back stages.

Equations

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

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackInclusion_fst {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) : CategoryStruct.comp (pullbackInclusion p F i) (Limits.pullback.fst p (F.toObject i.succ)) = Limits.pullback.fst p (F.toObject i.castSucc)

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackInclusion_fst_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (pullbackInclusion p F i) (CategoryStruct.comp (Limits.pullback.fst p (F.toObject i.succ)) h) = CategoryStruct.comp (Limits.pullback.fst p (F.toObject i.castSucc)) h

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackInclusion_snd {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) : CategoryStruct.comp (pullbackInclusion p F i) (Limits.pullback.snd p (F.toObject i.succ)) = CategoryStruct.comp (Limits.pullback.snd p (F.toObject i.castSucc)) (F.inclusion i)

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackInclusion_snd_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) {Z : C} (h : F.object i.succ ⟶ Z) : CategoryStruct.comp (pullbackInclusion p F i) (CategoryStruct.comp (Limits.pullback.snd p (F.toObject i.succ)) h) = CategoryStruct.comp (Limits.pullback.snd p (F.toObject i.castSucc)) (CategoryStruct.comp (F.inclusion i) h)

instance CategoryTheory.FiniteFiltration.pullbackInclusion_mono {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) : Mono (pullbackInclusion p F i)

noncomputable def CategoryTheory.FiniteFiltration.pullbackProjection {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) : pullbackObject p F i.succ ⟶ F.graded i

The quotient projection from a pulled-back stage.

Equations

• CategoryTheory.FiniteFiltration.pullbackProjection p F i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd p (F.toObject i.succ)) (F.projection i)

instance CategoryTheory.FiniteFiltration.pullbackProjection_epi {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) (i : Fin F.length) : Epi (pullbackProjection p F i)

theorem CategoryTheory.FiniteFiltration.pullback_zero {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) : CategoryStruct.comp (pullbackInclusion p F i) (pullbackProjection p F i) = 0

theorem CategoryTheory.FiniteFiltration.pullback_exact {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) (i : Fin F.length) : { X₁ := pullbackObject p F i.castSucc, X₂ := pullbackObject p F i.succ, X₃ := F.graded i, f := pullbackInclusion p F i, g := pullbackProjection p F i, zero := ⋯ }.Exact

noncomputable def CategoryTheory.FiniteFiltration.pullbackTower {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) : FiniteExactTower C

Pull a quotient filtration back along an epimorphism.

The result is an endpoint-free exact tower: its bottom is the kernel of p, while its top is canonically isomorphic to X. This is the actual refinement operation used when a coarse short exact step is replaced by a filtration of its quotient.

Equations

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

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackTower_length {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) : (pullbackTower p F).length = F.length

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackTower_object {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) (i : Fin ((pullbackTower p F).length + 1)) : (pullbackTower p F).object i = Limits.pullback p (F.toObject i)

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackTower_graded {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) (i : Fin (pullbackTower p F).length) : (pullbackTower p F).graded i = F.graded i

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackTower_gradedObjects {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) : (pullbackTower p F).gradedObjects = F.gradedObjects

noncomputable def CategoryTheory.FiniteFiltration.pullbackTowerInitialKernelFork {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) : Limits.KernelFork p

The bottom inclusion of the pullback tower, regarded as a kernel fork for p.

Equations

• CategoryTheory.FiniteFiltration.pullbackTowerInitialKernelFork p F = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.pullback.fst p (F.toObject 0)) ⋯

noncomputable def CategoryTheory.FiniteFiltration.pullbackTowerInitialIsLimit {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) (F : FiniteFiltration C Q) : Limits.IsLimit (pullbackTowerInitialKernelFork p F)

The bottom of the pullback tower is a kernel of p.

Equations

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

noncomputable def CategoryTheory.FiniteFiltration.pullbackTowerTerminalIso {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) : (pullbackTower p F).object (Fin.last (pullbackTower p F).length) ≅ X

The top of the pullback tower is canonically the source of the epimorphism.

Equations

• CategoryTheory.FiniteFiltration.pullbackTowerTerminalIso p F = id (CategoryTheory.asIso (CategoryTheory.Limits.pullback.fst p (F.toObject (Fin.last F.length))))

@[simp]

theorem CategoryTheory.FiniteFiltration.pullbackTowerTerminalIso_hom {C : Type u} [Category.{v, u} C] [Abelian C] {X Q : C} (p : X ⟶ Q) [Epi p] (F : FiniteFiltration C Q) : (pullbackTowerTerminalIso p F).hom = Limits.pullback.fst p (F.toObject (Fin.last F.length))

noncomputable def CategoryTheory.FiniteFiltration.refinementInitialIso {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (R : FiniteFiltration C (F.graded i)) : (pullbackTower (F.projection i) R).object 0 ≅ F.object i.castSucc

The bottom of the lifted refinement is canonically the preceding coarse stage.

Equations

• F.refinementInitialIso i R = (CategoryTheory.FiniteFiltration.pullbackTowerInitialIsLimit (F.projection i) R).conePointUniqueUpToIso ⋯.fIsKernel

noncomputable def CategoryTheory.FiniteFiltration.refinementTerminalIso {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (R : FiniteFiltration C (F.graded i)) : (pullbackTower (F.projection i) R).object (Fin.last (pullbackTower (F.projection i) R).length) ≅ F.object i.succ

The top of the lifted refinement is canonically the following coarse stage.

Equations

• F.refinementTerminalIso i R = CategoryTheory.FiniteFiltration.pullbackTowerTerminalIso (F.projection i) R

theorem CategoryTheory.FiniteFiltration.refinementInitialIso_hom_inclusion {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (R : FiniteFiltration C (F.graded i)) : CategoryStruct.comp (F.refinementInitialIso i R).hom (F.inclusion i) = Limits.pullback.fst (F.projection i) (R.toObject 0)

The initial comparison intertwines the lifted kernel inclusion and the coarse inclusion.

noncomputable def CategoryTheory.FiniteFiltration.refineStep {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (R : FiniteFiltration C (F.graded i)) : FiniteFiltration C M

Refine one graded quotient by pulling its filtration back to the adjacent coarse stages and splicing that exact tower into the original filtration.

Equations

• F.refineStep i R = F.spliceStep i (CategoryTheory.FiniteFiltration.pullbackTower (F.projection i) R) (F.refinementInitialIso i R) (F.refinementTerminalIso i R)

@[simp]

theorem CategoryTheory.FiniteFiltration.refineStep_length {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (R : FiniteFiltration C (F.graded i)) : (F.refineStep i R).length = F.length - 1 + R.length

@[simp]

theorem CategoryTheory.FiniteFiltration.refineStep_gradedObjects {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (i : Fin F.length) (R : FiniteFiltration C (F.graded i)) : (F.refineStep i R).gradedObjects = List.take (↑i) F.gradedObjects ++ R.gradedObjects ++ List.drop (↑i + 1) F.gradedObjects

noncomputable def CategoryTheory.FiniteFiltration.refineAll {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (R : (i : Fin F.length) → FiniteFiltration C (F.graded i)) : FiniteFiltration C M

Refine every graded quotient of a filtration at once.

For each coarse step, its quotient filtration is pulled back to an exact tower between the adjacent coarse stages. FiniteExactTower.replaceSteps then concatenates those lifted towers in coarse-step order. This is the categorical refinement used in the composition argument for almost-disconnected morphisms.

Equations

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

@[simp]

theorem CategoryTheory.FiniteFiltration.refineAll_length {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (R : (i : Fin F.length) → FiniteFiltration C (F.graded i)) : (F.refineAll R).length = (List.ofFn fun (i : Fin F.length) => (R i).length).sum

@[simp]

theorem CategoryTheory.FiniteFiltration.refineAll_gradedObjects {C : Type u} [Category.{v, u} C] [Abelian C] {M : C} (F : FiniteFiltration C M) (R : (i : Fin F.length) → FiniteFiltration C (F.graded i)) : (F.refineAll R).gradedObjects = (List.ofFn fun (i : Fin F.length) => (R i).gradedObjects).flatten