Relative Harder--Narasimhan filtrations over curve bases

This file replaces the proposition-valued Dedekind-HN placeholder at the scheme-facing boundary with object-level data. A SchemeRelativeHNFiltration is an actual HNFiltration of an object in the category over a scheme base change. Its tower, factors, strictly decreasing phases, and semistability proofs are exposed directly.

Given the explicit FiberPreStabilityBaseChangeData witness, the filtration pulls back along every morphism of scheme base changes. Specializing to the canonical residue-field morphism produces an ordinary HNFiltration in the point fiber, with the same length and phases and factors obtained by actual categorical pullback.

RegularCurveBaseChange packages a genuine scheme over the fixed base whose scheme is Noetherian, whose local rings are regular of dimension at most one, and which has a point of local dimension one. An additional predicate remains available in schemeRelativeHNProblem for the source's essentially-finite-type or other eligibility conditions.

Existence for a general geometric family is deliberately retained as the named premise HasSchemeRelativeHNFiltrations. The constant categorical family is inhabited using the HN existence field of its slicing. No semistable reduction, bounded coherent/perfect realization, moduli construction, or conclusion of Theorem 22.2 is asserted.

structure AlgebraicGeometry.Moduli.HarderNarasimhan.RegularCurveBaseChange (S : Scheme) : Type (u + 1)

An actual scheme base change whose underlying scheme has the local properties of a regular one-dimensional Noetherian curve.

• baseChange : DerivedCategory.Families.SchemeBaseChange S

  The actual scheme over S.

• noetherian : IsNoetherian (CategoryTheory.Over.left self.baseChange)

  The curve is Noetherian.

• regular (x : ↥(CategoryTheory.Over.left self.baseChange)) : IsRegularLocalRing ↑((CategoryTheory.Over.left self.baseChange).presheaf.stalk x)

  Every local ring is regular.

• dimensionLEOne (x : ↥(CategoryTheory.Over.left self.baseChange)) : Ring.KrullDimLE 1 ↑((CategoryTheory.Over.left self.baseChange).presheaf.stalk x)

  Every local ring has Krull dimension at most one.

• hasDimensionOne : ∃ (x : ↥(CategoryTheory.Over.left self.baseChange)), ¬Ring.KrullDimLE 0 ↑((CategoryTheory.Over.left self.baseChange).presheaf.stalk x)

  At least one local ring has positive dimension, excluding the zero-dimensional case.

instance AlgebraicGeometry.Moduli.HarderNarasimhan.RegularCurveBaseChange.instIsNoetherianLeftSchemeBaseChange {S : Scheme} (T : RegularCurveBaseChange S) : IsNoetherian (CategoryTheory.Over.left T.baseChange)

instance AlgebraicGeometry.Moduli.HarderNarasimhan.RegularCurveBaseChange.instIsRegularLocalRingCarrierStalkCommRingCatPresheafLeftSchemeBaseChange {S : Scheme} (T : RegularCurveBaseChange S) (x : ↥(CategoryTheory.Over.left T.baseChange)) : IsRegularLocalRing ↑((CategoryTheory.Over.left T.baseChange).presheaf.stalk x)

instance AlgebraicGeometry.Moduli.HarderNarasimhan.RegularCurveBaseChange.instKrullDimLEOfNatNatCarrierStalkCommRingCatPresheafLeftSchemeBaseChange {S : Scheme} (T : RegularCurveBaseChange S) (x : ↥(CategoryTheory.Over.left T.baseChange)) : Ring.KrullDimLE 1 ↑((CategoryTheory.Over.left T.baseChange).presheaf.stalk x)

structure AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration {S : Scheme} (F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S) {V : Type uV} [AddCommGroup V] (classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V) (sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)) {T : DerivedCategory.Families.SchemeBaseChange S} (E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) : Type (max u u_1)

An object-level relative HN filtration over an actual scheme base change. The underlying HNFiltration contains the finite Postnikov tower, factors, strict phase ordering, and phase-slice membership.

• filtration : CategoryTheory.Triangulated.HNFiltration (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (sigma T).slicing.P E

  The actual HN filtration in the category over the base change.

• fiberFiltration (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Triangulated.HNFiltration (F.ResidueFiber T x) (sigma (T.residue x)).slicing.P ((F.pullToResidue T x).obj E)

  The ordinary HN filtration obtained at every actual residue fiber.

• fiber_length (x : ↥(CategoryTheory.Over.left T)) : (self.fiberFiltration x).n = self.filtration.n

  Fiber restriction preserves the number of factors.

• fiber_phase (x : ↥(CategoryTheory.Over.left T)) (i : Fin self.filtration.n) : (self.fiberFiltration x).φ (Fin.cast ⋯ i) = self.filtration.φ i

  Fiber restriction preserves every factor phase.

• fiberFactorIso (x : ↥(CategoryTheory.Over.left T)) (i : Fin self.filtration.n) : (self.fiberFiltration x).factor (Fin.cast ⋯ i) ≅ (F.pullToResidue T x).obj (self.filtration.factor i)

  Each fiber factor is the actual pullback of its relative factor.

def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.tower {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) : CategoryTheory.Triangulated.PostnikovTower (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) E

The finite Postnikov tower underlying a relative HN filtration.

Equations

• H.tower = H.filtration.toPostnikovTower

def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.length {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) : ℕ

The number of relative semistable factors.

Equations

• H.length = H.filtration.n

def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.factor {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (i : Fin H.length) : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T

The i-th relative factor.

Equations

• H.factor i = H.filtration.factor i

def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.phase {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (i : Fin H.length) : ℝ

The phase of the i-th relative factor.

Equations

• H.phase i = H.filtration.φ i

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.phase_strictAnti {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) : StrictAnti H.phase

Relative factor phases are strictly decreasing.

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.factor_semistable {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (i : Fin H.length) : (sigma T).slicing.P (H.phase i) (H.factor i)

Every relative factor lies in its recorded phase slice.

def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.fiberIndex {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (x : ↥(CategoryTheory.Over.left T)) (i : Fin H.length) : Fin (H.fiberFiltration x).n

Reindex a relative factor by the equality of relative and point-fiber lengths.

Equations

• H.fiberIndex x i = Fin.cast ⋯ i

noncomputable def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.ofBaseChangeWitness {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (filtration : CategoryTheory.Triangulated.HNFiltration (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (sigma T).slicing.P E) (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) : SchemeRelativeHNFiltration F classMap sigma E

Construct coherent relative data from an HN filtration over the base change and the explicit geometric preimage-slicing witness.

Equations

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

noncomputable def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.pullback {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) {U : DerivedCategory.Families.SchemeBaseChange S} (f : U ⟶ T) : SchemeRelativeHNFiltration F classMap sigma ((CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F f).obj E)

Pull an object-level relative HN filtration along a morphism of scheme base changes. The geometric slicing witness supplies semistability of the pulled-back factors.

Equations

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

@[simp]

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.pullback_length {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) {U : DerivedCategory.Families.SchemeBaseChange S} (f : U ⟶ T) : (H.pullback h f).length = H.length

@[simp]

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.pullback_phase {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) {U : DerivedCategory.Families.SchemeBaseChange S} (f : U ⟶ T) (i : Fin H.length) : (H.pullback h f).phase i = H.phase i

noncomputable def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.pullbackFactorIso {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) {U : DerivedCategory.Families.SchemeBaseChange S} (f : U ⟶ T) (i : Fin H.length) : (H.pullback h f).factor i ≅ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.pull F f).obj (H.factor i)

Each factor of the pulled-back filtration is the actual pullback of the corresponding relative factor.

Equations

• H.pullbackFactorIso h f i = CategoryTheory.Iso.refl ((H.pullback h f).factor i)

noncomputable def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.restrictToFiber {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (x : ↥(CategoryTheory.Over.left T)) : CategoryTheory.Triangulated.HNFiltration (F.ResidueFiber T x) (sigma (T.residue x)).slicing.P ((F.pullToResidue T x).obj E)

Restriction of a relative filtration to a point is an ordinary HN filtration in the actual residue fiber.

Equations

• H.restrictToFiber x = H.fiberFiltration x

@[simp]

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.restrictToFiber_length {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (x : ↥(CategoryTheory.Over.left T)) : (H.restrictToFiber x).n = H.length

@[simp]

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.restrictToFiber_phase {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (x : ↥(CategoryTheory.Over.left T)) (i : Fin H.length) : (H.restrictToFiber x).φ (H.fiberIndex x i) = H.phase i

def AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.restrictToFiberFactorIso {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (x : ↥(CategoryTheory.Over.left T)) (i : Fin H.length) : (H.restrictToFiber x).factor (H.fiberIndex x i) ≅ (F.pullToResidue T x).obj (H.factor i)

The factor in the point-fiber HN filtration is the pullback of the relative factor.

Equations

• H.restrictToFiberFactorIso x i = H.fiberFactorIso x i

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.pullback_comp_phase {S : Scheme} {F : DerivedCategory.Families.SchemeTriangulatedFiberFamily S} {V : Type uV} [AddCommGroup V] {classMap : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.K₀ (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) →+ V} {sigma : (T : DerivedCategory.Families.SchemeBaseChange S) → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap (CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T) (classMap T)} {T : DerivedCategory.Families.SchemeBaseChange S} {E : CategoryTheory.Triangulated.Families.TriangulatedFiberFamily.Fiber F T} (H : SchemeRelativeHNFiltration F classMap sigma E) (h : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Families.FiberPreStabilityBaseChangeData F classMap sigma) {R U : DerivedCategory.Families.SchemeBaseChange S} (f : R ⟶ U) (g : U ⟶ T) (i : Fin H.length) : (H.pullback h (CategoryTheory.CategoryStruct.comp f g)).phase i = ((H.pullback h g).pullback h f).phase i

Direct pullback and two-stage pullback preserve the same phase function. This is the filtration-level numerical coherence supplied by the contravariant family and the compositional slicing witness.

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.SchemeRelativeHNFiltration.constant_nonempty (S : Scheme) (C : Type w) [CategoryTheory.Category.{w, w} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (V : Type uV) [AddCommGroup V] (v₀ : CategoryTheory.Triangulated.K₀ C →+ V) (sigma₀ : CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap C v₀) (T : DerivedCategory.Families.SchemeBaseChange S) (E : C) : Nonempty (SchemeRelativeHNFiltration (DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant S C) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => v₀) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => sigma₀) E)

One ordinary HN filtration supplies an object-level relative filtration in a constant categorical family over any actual scheme base change.