Relative Harder--Narasimhan realizations of categorical family interfaces

The geometric filtration lives in RelativeFiltration.lean. This file packages it as the generic DedekindHNProblem and its integration predicate. It lives with the geometric object it is about, not below the categorical interface it implements.

def AlgebraicGeometry.Moduli.HarderNarasimhan.schemeRelativeHNProblem {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)) (IsEligible : RegularCurveBaseChange S → Prop) : CategoryTheory.Triangulated.WeakStabilityCondition.Families.DedekindHNProblem (RegularCurveBaseChange S)

The categorical Dedekind-HN problem realized by regular curve base changes and object-level relative HN filtrations.

Equations

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

def AlgebraicGeometry.Moduli.HarderNarasimhan.HasSchemeRelativeHNFiltrations {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)) (IsEligible : RegularCurveBaseChange S → Prop) : Prop

Objectwise existence of relative HN filtrations on eligible curve bases.

Equations

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

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.integratesAfterDedekindBaseChange_of_relativeHN {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)) {IsEligible : RegularCurveBaseChange S → Prop} (h : HasSchemeRelativeHNFiltrations F classMap sigma IsEligible) : CategoryTheory.Triangulated.WeakStabilityCondition.Families.IntegratesAfterDedekindBaseChange (schemeRelativeHNProblem F classMap sigma IsEligible)

Objectwise relative-HN existence realizes the categorical integration clause.

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.hasSchemeRelativeHNFiltrations_constant (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₀) (IsEligible : RegularCurveBaseChange S → Prop) : HasSchemeRelativeHNFiltrations (DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant S C) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => v₀) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => sigma₀) IsEligible

The constant categorical family realizes relative-HN existence.

theorem AlgebraicGeometry.Moduli.HarderNarasimhan.integratesAfterDedekindBaseChange_relativeHN_constant (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₀) (IsEligible : RegularCurveBaseChange S → Prop) : CategoryTheory.Triangulated.WeakStabilityCondition.Families.IntegratesAfterDedekindBaseChange (schemeRelativeHNProblem (DerivedCategory.Families.SchemeTriangulatedFiberFamily.constant S C) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => v₀) (fun (x : DerivedCategory.Families.SchemeBaseChange S) => sigma₀) IsEligible)

The constant family consequently realizes categorical Dedekind integration.