HarderNarasimhan

A Lean 4 formalization of the Harder–Narasimhan Games of Huayi Chen & Marion Jeannin: a two-player game played on the strict intervals of a bounded lattice. The library develops Harder–Narasimhan filtrations, Jordan–Hölder filtrations, and coprimary filtrations of nonzero finitely generated modules over a Noetherian commutative ring.

Mathematical overview

The central object is a payoff function: a bundled structure

structure PayoffFunction (ℒ : Type*) [LT ℒ] (S : Type*) where
  toFun : StrictIntvl ℒ → S

assigning to each strict interval (a, b) (with a < b) of an order ℒ a payoff in a complete lattice S. Everything else is accessed through dot notation on μ:

• μ.max I — the supremum over I.left < u ≤ I.right, with the left endpoint fixed;
• μ.min I — the infimum over I.left ≤ u < I.right, with the right endpoint fixed;
• μ.A I / μ.B I — the game values when player A or player B moves first, respectively;
• μ.restrict I — the induced payoff function on the points ↥I of a subinterval;
• μ.dual — the order-dual payoff function, exchanging the two players;
• μ.IsConvex, μ.IsSlopeLike, μ.IsSemistable, … — typeclass hypotheses on μ;
• μ.breakpoints I — the canonical cut points from which filtrations are built;
• μ.hnFiltration — the canonical Harder–Narasimhan filtration of μ.

Under suitable chain and slope-like conditions, the game values satisfy μ.A ⊤ = μ.min ⊤ and μ.B ⊤ = μ.max ⊤. For linearly ordered slope-like payoffs with the required chain conditions on restrictions, Nash equilibrium is equivalent to semistability. For convex admissible payoffs satisfying the ascending chain condition and ADCC, iterating greatest breakpoints gives a Harder–Narasimhan filtration, unique when the payoff order is linear. Applying this construction to associated primes of subquotients gives coprimary filtrations, relative to a fixed linear extension of the prime spectrum.

Library structure

Importing HarderNarasimhan (the umbrella module HarderNarasimhan.lean) brings in the whole library. It is organized as one infrastructure file and four blocks:

Infrastructure

• HarderNarasimhan/StrictIntvl.lean — the type StrictIntvl ℒ of strict intervals left < right, its inclusion order and top element, and the points type ↥I with its inherited BoundedOrder/Lattice/IsModularLattice/ WellFoundedGT instances.

PayoffFunction/ — the game and its values

• Defs.lean — the PayoffFunction structure, the operations max/min/A/B and their basic API, IsAttained, and the order dual.
• Restrict.lean — restriction to a subinterval and its commutation with max/min/A/B.
• Convex.lean — the convexity classes IsConvex/IsConvexOn/IsAffine and the fundamental inequalities for μ.A.
• Semistable/Defs.lean — IsSemistable/IsStable, the chain condition ADCC, and breakpoints.
• Semistable/Breakpoints.lean — existence, uniqueness, totality, and the decomposition formula for breakpoints.
• SlopeLike.lean — the slope-like axiom and its seesaw trichotomy (seesaw_* iff family).
• Slope.lean — the prototypical slope-like payoff slope r d (degree over rank, valued in a Dedekind–MacNeille completion).
• GameValue.lean — chain conditions (WeakACC, StrongDCC), computation of the global game values, first-mover advantage.
• NashEquilibrium.lean — HasNashEquilibrium and its equivalence with semistability.

Filtration/ — Harder–Narasimhan filtrations

• Defs.lean — the HarderNarasimhanFiltration structure (explicit length, semistable steps, and successive μ.A-values satisfying ¬ aᵢ ≤ aᵢ₊₁, or strict decrease for a linear codomain) and the Admissible side condition.
• Exists.lean — the canonical construction μ.hnFiltration by iterated greatest breakpoints.
• Unique.lean — uniqueness over a complete linear order, and the RelSeries repackaging.

JordanHolder/ — Jordan–Hölder filtrations

• Defs.lean — the JordanHolderFiltration structure (descending chains with total step payoff) and the chain condition EventuallyTopDCC.
• Exists.lean — existence by successively choosing maximal points with the required payoff (a Nonempty instance; uniqueness is not asserted).
• Stability.lean — the step condition is equivalent to piecewise stability of the restricted payoffs.
• Length.lean — for semistable slope-like affine payoffs in a complete linear order, Jordan–Hölder filtrations on a modular lattice have the same length under the existence hypotheses.

Coprimary/ — coprimary filtrations of modules

• AssociatedPrimes.lean — pure commutative algebra: associated primes of the quotient by a localization kernel (Bourbaki, Algèbre commutative).
• Defs.lean — the coprimary payoff function Coprimary.payoff R M on the submodule lattice, IsCoprimary, and the CoprimaryFiltration structure.
• Semistability.lean — explicit computation of the value when A moves first; semistability is having a unique associated prime.
• Filtration.lean — existence and uniqueness of the coprimary filtration, via the general Harder–Narasimhan machinery.

The dependency graph HarderNarasimhan.json (linked in the badge above) is regenerated by a local development script that is not tracked in this repository.

How to read this repository

1. Start with StrictIntvl.lean and PayoffFunction/Defs.lean for the two core types and the game values.
2. Read Convex.lean and the two Semistable/ files for the breakpoint machinery — the heart of the theory.
3. Filtration/Exists.lean and Filtration/Unique.lean assemble the main theorem on Harder–Narasimhan filtrations.
4. The game-theoretic side (GameValue.lean, NashEquilibrium.lean) and the JordanHolder/ block can be read independently after step 2.
5. Coprimary/ shows the abstract theory at work on an honest example from commutative algebra.

Main results at a glance

Declarations live in the namespace HarderNarasimhan.PayoffFunction unless qualified otherwise. Results that are naturally packaged as conjunctions or TFAE blocks are split into the listed single-conclusion lemmas.

Result	Lean declaration(s)
Fundamental inequality chain for convex payoff functions	A_le_max_inf, IsConvexOn.max_inf_le_max, IsConvexOn.A_le_A_sup
Stability of the extremal operations under convexity	IsConvexOn.max, IsConvexOn.max_max, IsConvexOn.A_max
Comparison of μ.A-values along a chain	A_anti_left, IsConvexOn.inf_le_A, IsConvexOn.A_eq_of_ge, IsConvexOn.A_le_A_of_lt, IsConvexOn.A_eq_or_lt
Complementary segment value after a strict improvement	IsConvex.A_right_eq_of_A_left_gt
Comparison of μ.A-values along a join	IsConvexOn.inf_A_le_A_sup, IsConvexOn.A_le_A_sup_or
Interval enlargement when the μ.A-value is ⊤	IsConvexOn.A_le_of_A_eq_top
Sufficient condition for the descending chain condition	adcc_of_exists_A_eq_top
Existence of breakpoints	breakpoints_nonempty
Uniqueness of the breakpoint over a complete linear order	IsBreakpoint.eq
Semistability below and obstruction above a breakpoint	IsBreakpoint.isSemistable_restrict, IsBreakpoint.not_A_le
Totality, greatest element, and decomposition for breakpoints	breakpoints_total, exists_isGreatest_breakpoints, IsBreakpoint.A_eq_A_of_lt
Existence and uniqueness of the Harder–Narasimhan filtration	hnFiltration, Unique (μ.HarderNarasimhanFiltration), exists_relSeries_semistableRel, existsUnique_relSeries_semistableRel
Equalities of μ.A-values along the canonical filtration	hnFiltration_A_bot_eq_A
Convexity of the coprimary payoff function	the IsConvexOn ⊤ instance for Coprimary.payoff R M
Value of the coprimary payoff function when A moves first	Coprimary.A_payoff
Descending chain condition for the coprimary payoff function	the ADCC instance for Coprimary.payoff R M
Semistable means coprimary	Coprimary.isSemistable_iff_A_const, Coprimary.isSemistable_iff_existsUnique_associatedPrime
Existence and uniqueness of the coprimary filtration	Coprimary.coprimaryFiltration, Unique (CoprimaryFiltration R M)
The associated primes of M via the coprimary filtration	CoprimaryFiltration.associatedPrimes_eq_iUnion
Player A's value equals the global infimum	A_top_eq_min_top, A_top_le_B_top
Player B's value equals the global supremum	B_top_eq_max_top, A_top_le_B_top_of_strongDCC
Strong descending chain condition from a well-ordered rank	strongDCC_of_wellOrderedRank
The slope-like axiom as the seesaw trichotomy	isSlopeLike_iff_seesaw, IsSlopeLike.seesaw
The slope of a degree by a rank is slope-like	isSlopeLike_slope
Unfolded reformulations of the equilibrium condition	min_le_apply, apply_le_max, B_top_le_A_top_iff, hasNashEquilibrium_iff_min_le, hasNashEquilibrium_iff_le_max
Equilibrium inequality vs. coincidence of the extremal values	B_top_le_A_top_of_min_eq_max, min_top_eq_max_top_of_B_top_le_A_top
Equivalence of the endpoint equalities for slope-like payoffs	max_top_eq_apply_iff, min_top_eq_apply_iff
Semistability implies Nash equilibrium	IsSemistable.B_top_le_A_top, IsSemistable.hasNashEquilibrium
Nash equilibrium implies semistability	isSemistable_of_hasNashEquilibrium
Nash equilibrium iff the global extremal values coincide	min_top_eq_max_top_iff_hasNashEquilibrium, nashEquilibrium_tfae
Existence of Jordan–Hölder filtrations	Nonempty (μ.JordanHolderFiltration), exists_relSeries_jordanHolderRel

Further results include the uniqueness of the Jordan–Hölder length under the hypotheses above (JordanHolderFiltration.length_eq), the piecewise-stability characterization (piecewise_isStable_iff), and the commutative algebra input HarderNarasimhan.associatedPrimes_quot_ker_mkLinearMap.

Building

The repository pins Lean and mathlib via lean-toolchain and lakefile.toml:

lake exe cache get   # fetch the mathlib build cache
lake build

License

Licensed under the Apache License, Version 2.0. See LICENSE.