Mass--Hom bounds #
For a stability condition σ and a property T of test objects, a mass--Hom
bound says that every A ∈ T admits a positive constant K_A such that
dim_k Hom(A, F) ≤ K_A m_σ(F)
for every object F. Taking T = ⊤ is Halpern--Leistner--Robotis,
Definition 2.7; for a proper scheme the intended geometric test class is
Perf(X).
The constant is existential rather than data. Hom-finiteness is an explicit ambient hypothesis: this abstract file neither supplies it nor derives it from triangulated structure.
This file also records the formal invariances needed downstream. Isomorphisms
and simultaneous shifts preserve both sides exactly. Compatible k-linear
autoequivalences preserve mass exactly while transporting the test class.
The lifted GL⁺(2, ℝ) action fixes objects and changes mass by a uniform
operator-norm factor.
A mass--Hom bound for one test object. The positive constant is a propositionally existential witness, not chosen data.
The HomFinite argument is intentionally explicit even though finrank is
junk-total without it; the declaration-level lint exception prevents that
mathematical guard from being erased as a syntactically unused argument.
Equations
- σ.HasMassHomBoundFor A = ∃ (K : ℝ), 0 < K ∧ ∀ (F : C), ↑(Module.finrank k (A ⟶ F)) ≤ K * (CategoryTheory.Triangulated.stabilityMass σ F).toReal
Instances For
A mass--Hom bound on a property T of test objects.
Equations
- σ.HasMassHomBound T = ∀ (A : C), T A → σ.HasMassHomBoundFor A
Instances For
The original all-object form of the mass--Hom bound.
Equations
Instances For
Restricting the test class preserves a mass--Hom bound.
The all-object spelling exposes the same objectwise predicate.
The pointwise inequality is invariant under isomorphism of both the test and target objects.
A mass--Hom bound depends on its test object only up to isomorphism.
On a semistable object the mass--Hom inequality has the normal form
dim Hom(A,F) ≤ K_A ‖Z(F)‖.
Simultaneously shifting both variables by one preserves a mass--Hom inequality.
Simultaneously shifting both variables by minus one preserves a mass--Hom inequality.
Shifting the test object by one preserves a mass--Hom bound.
Shifting the test object by minus one preserves a mass--Hom bound.
Compatible autoequivalences #
A compatible k-linear autoequivalence transports a mass--Hom bound to
the canonical inverse-image test property.
Autoequivalence transport is an equivalence for a replete test class. The right side uses the canonical inverse-image property rather than a second chosen presentation of the transported class.
The lifted GL⁺(2, ℝ) action #
Relabel an HN filtration along an arbitrary lifted linear action. The tower and factors are unchanged; only the phases are transported.
Equations
- CategoryTheory.Triangulated.HNFiltration.relabelStability x σ F = { toPostnikovTower := F.toPostnikovTower, φ := fun (i : Fin F.n) => x.shift.toOrderIso (F.φ i), hφ := ⋯, semistable := ⋯ }
Instances For
A strictly positive uniform expansion factor for the complex-plane action.
The harmless added 1 avoids exposing invertibility bookkeeping at every
mass--Hom consumer.
Equations
Instances For
The lifted linear action expands every real HN mass by at most
glMassBound x.
The original mass is controlled by the mass after a lifted linear action, using the expansion factor of the inverse element.
A lifted linear action preserves the mass--Hom property, with constants rescaled by the uniform inverse expansion factor.
The mass--Hom property is invariant under the lifted linear group action.