Lifting a filtration of a quotient back to the ambient object

The Harder–Narasimhan recursion removes the maximal destabilizing subobject B ⊆ E, filters the quotient E / B, and splices the two together. This file supplies the lattice-level facts that splice needs, all of them about the subobject correspondence and none of them about slopes.

• pullback_bot — the bottom subobject of E / B pulls back to B itself, so the spliced chain really does begin ⊥ < B < …. It is pullback_imageSubobject_eq at S = B, where the image of B.arrow ≫ cokernel.π B.arrow = 0 is ⊥.
• pullback_lt_of_lt — strict inclusions pull back to strict inclusions. This is not formal monotonicity: it is proved from the fact that a chain step with a nonzero successive quotient cannot be an equality, using cokernelPullbackIso to identify that quotient with the one upstairs.
• cokernelOfLEBotIso — the first successive quotient of the spliced chain, cokernel (⊥ ⟶ B), is B itself, which is what lets the first factor's slope and semistability be read off the maximal destabilizing subobject.

Nothing here mentions a polarization; it is the correspondence, specialised to what the splice consumes.

theorem AlgebraicGeometry.Stability.Gieseker.pullback_bot {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) : (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.cokernel.π B.arrow)).obj ⊥ = B

The bottom of the quotient pulls back to the subobject itself.

theorem AlgebraicGeometry.Stability.Gieseker.ofLE_bot_eq_zero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) (h : ⊥ ≤ B) : ⊥.ofLE B h = 0

The inclusion of the bottom subobject into any subobject is the zero morphism.

noncomputable def AlgebraicGeometry.Stability.Gieseker.cokernelOfLEBotIso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) (h : ⊥ ≤ B) : CategoryTheory.Limits.cokernel (⊥.ofLE B h) ≅ CategoryTheory.Subobject.underlying.obj B

The first successive quotient of a spliced chain is the subobject itself.

Equations

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

theorem AlgebraicGeometry.Stability.Gieseker.cokernel_not_isZero_of_lt {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {Y : Coh X} {C₁ C₂ : CategoryTheory.Subobject Y} (hlt : C₁ < C₂) : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel (C₁.ofLE C₂ ⋯))

A strict inclusion of subobjects has a nonzero successive quotient: a zero cokernel would make the inclusion an isomorphism. This is AbelianWeakHNFiltration.factor_not_isZero's argument, stated for a bare pair of subobjects.

theorem AlgebraicGeometry.Stability.Gieseker.pullback_lt_of_lt {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) {C₁ C₂ : CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)} (hlt : C₁ < C₂) : (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.cokernel.π B.arrow)).obj C₁ < (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.cokernel.π B.arrow)).obj C₂

Strict inclusions pull back to strict inclusions.

Monotonicity is formal; strictness is not. If the pullbacks agreed, the inclusion between them would be an isomorphism and its cokernel zero, but cokernelPullbackIso identifies that cokernel with the successive quotient upstairs, which a strict inclusion makes nonzero.

noncomputable def AlgebraicGeometry.Stability.Gieseker.cokernelOfLECongr {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {Y : Coh X} {C₁ C₂ C₁' C₂' : CategoryTheory.Subobject Y} (hle : C₁ ≤ C₂) (hle' : C₁' ≤ C₂') (e₁ : C₁ = C₁') (e₂ : C₂ = C₂') : CategoryTheory.Limits.cokernel (C₁.ofLE C₂ hle) ≅ CategoryTheory.Limits.cokernel (C₁'.ofLE C₂' hle')

Transport of a successive quotient along equalities of its endpoints. The inclusion's proof argument is irrelevant, so the two cokernels agree once the endpoints do.

Equations

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

noncomputable def AlgebraicGeometry.Stability.Gieseker.spliceChain {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) {m : ℕ} (c : Fin (m + 1) → CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) : Fin (m + 1 + 1) → CategoryTheory.Subobject F

The spliced chain: the bottom subobject, then the pullbacks of a chain in the quotient.

Equations

• AlgebraicGeometry.Stability.Gieseker.spliceChain B c i = Fin.cases ⊥ (fun (j : Fin (m + 1)) => (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.cokernel.π B.arrow)).obj (c j)) i

@[simp]

theorem AlgebraicGeometry.Stability.Gieseker.spliceChain_zero {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) {m : ℕ} (c : Fin (m + 1) → CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) : spliceChain B c 0 = ⊥

@[simp]

theorem AlgebraicGeometry.Stability.Gieseker.spliceChain_succ {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) {m : ℕ} (c : Fin (m + 1) → CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) (j : Fin (m + 1)) : spliceChain B c j.succ = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.cokernel.π B.arrow)).obj (c j)

theorem AlgebraicGeometry.Stability.Gieseker.spliceChain_strictMono {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} {B : CategoryTheory.Subobject F} (hB : ¬CategoryTheory.Limits.IsZero (CategoryTheory.Subobject.underlying.obj B)) {m : ℕ} {c : Fin (m + 1) → CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)} (hc : StrictMono c) (hbot : c 0 = ⊥) : StrictMono (spliceChain B c)

The spliced chain is strictly monotone: the first step is ⊥ < B, which needs B nonzero, and every later step is a pullback of a strict step downstairs.

theorem AlgebraicGeometry.Stability.Gieseker.spliceChain_top {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) {m : ℕ} (c : Fin (m + 1) → CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) (htop : c (Fin.last m) = ⊤) : spliceChain B c (Fin.last (m + 1)) = ⊤

The spliced chain ends at the top, because the pullback of the top subobject is the top.

noncomputable def AlgebraicGeometry.Stability.Gieseker.spliceFactorZeroIso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) {m : ℕ} (c : Fin (m + 1) → CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) (hbot : c 0 = ⊥) (hle : spliceChain B c (Fin.castSucc 0) ≤ spliceChain B c (Fin.succ 0)) : CategoryTheory.Limits.cokernel ((spliceChain B c (Fin.castSucc 0)).ofLE (spliceChain B c (Fin.succ 0)) hle) ≅ CategoryTheory.Subobject.underlying.obj B

The first factor of a spliced chain is the subobject itself.

Equations

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

noncomputable def AlgebraicGeometry.Stability.Gieseker.spliceFactorSuccIso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {F : Coh X} (B : CategoryTheory.Subobject F) {m : ℕ} (c : Fin (m + 1) → CategoryTheory.Subobject (CategoryTheory.Limits.cokernel B.arrow)) (j : Fin m) (hle : spliceChain B c j.succ.castSucc ≤ spliceChain B c j.succ.succ) (hlec : c j.castSucc ≤ c j.succ) : CategoryTheory.Limits.cokernel ((spliceChain B c j.succ.castSucc).ofLE (spliceChain B c j.succ.succ) hle) ≅ CategoryTheory.Limits.cokernel ((c j.castSucc).ofLE (c j.succ) hlec)

Every later factor of a spliced chain is the corresponding factor downstairs.

Equations

• AlgebraicGeometry.Stability.Gieseker.spliceFactorSuccIso B c j hle hlec = AlgebraicGeometry.Stability.Gieseker.cokernelOfLECongr hle ⋯ ⋯ ⋯ ≪≫ CategoryTheory.Abelian.cokernelPullbackIso B hlec

noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.firstFactorIso {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {Y : Coh X} (G : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction Y) : G.factor ⟨0, ⋯⟩ ≅ CategoryTheory.Subobject.underlying.obj (G.chain ⟨0, ⋯⟩.succ)

The first factor of a filtration is its first chain step.

The opening successive quotient runs out of the bottom subobject, so it is the first chain step itself. This is what turns a statement about the subobjects of a quotient into one about the factors of a filtration of it.

Equations

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

theorem AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.muZero_lt_topSlope {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {F : Coh X} {B : CategoryTheory.Subobject F} (hB : IsMaximalDestabilizing h F B) (G : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction (CategoryTheory.Limits.cokernel B.arrow)) : G.μ ⟨0, ⋯⟩ < (P.weakSlopeData h).topSlope (CategoryTheory.Subobject.underlying.obj B)

The top slope of a filtration of the quotient lies strictly below the maximal slope.

The first factor is a genuine nonzero subobject of the quotient, so the strict drop applies to it. This is the inequality that makes the spliced slope vector strictly antitone at the splice point, and it is the only place the drop is needed.

noncomputable def AlgebraicGeometry.Stability.Gieseker.PolarizedVarietyData.splice {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] {P : PolarizedVarietyData k X} (h : MuPositivityData P) {F : Coh X} {B : CategoryTheory.Subobject F} (hB : IsMaximalDestabilizing h F B) (G : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction (CategoryTheory.Limits.cokernel B.arrow)) : CategoryTheory.Triangulated.AbelianWeakHNFiltration (P.weakSlopeData h).toWeakStabilityFunction F

The spliced Harder–Narasimhan filtration.

Given the maximal destabilizing subobject B ⊆ F and a filtration of F / B, prepend B. The chain is spliceChain, the slope vector is the slope of B followed by the quotient's, and every field is one of the facts above:

• strict monotonicity is spliceChain_strictMono;
• strict antitonicity is muZero_lt_topSlope at the splice point and G.μ_anti above it. It is proved directly rather than through the adjacent-step criterion, because that criterion would index by Fin G.n with G.n opaque, which cannot be case-split;
• the factors are identified by spliceFactorZeroIso and spliceFactorSuccIso, and their slopes and semistability transported along those isomorphisms.

Equations

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