Mass--Hom bounds over finite-type field extensions

This file isolates the cancellation in inequality (8.4) of arXiv:2607.28411v1, Theorem 8.23. A finite-type extension of fields is finite by Zariski's lemma. The remaining two geometric inputs are stated exactly as the formulas used in the paper:

• adjunction and restriction of scalars multiply the extension-field Hom dimension by the degree of the extension;
• pushforward of the base-changed HN filtration multiplies mass by the same degree.

The theorem cancels this positive common factor. It does not manufacture either formula or a scalar-base-change stability condition; those are the geometric outputs of the Theorem 2.8 lane.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.UniformMassHomBound {J : Type u_1} (dimension : J → ℕ) (mass : J → ℝ) : Prop

A uniform numerical mass--Hom estimate on an arbitrary index of field/object tests. This is the common codomain of the cancellation theorem below and HLR Theorem 2.35(1).

Equations

• CategoryTheory.Triangulated.StabilityCondition.WithClassMap.UniformMassHomBound dimension mass = ∃ (K : ℝ), 0 < K ∧ ∀ (j : J), ↑(dimension j) ≤ K * mass j

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.UniformMassHomBound.of_scaled {J : Type u_1} {baseDimension dimension : J → ℕ} {baseMass mass degree : J → ℝ} (hdegree : ∀ (j : J), 0 < degree j) (hbase : UniformMassHomBound baseDimension baseMass) (hadjunction : ∀ (j : J), degree j * ↑(dimension j) = ↑(baseDimension j)) (hHNMass : ∀ (j : J), baseMass j = degree j * mass j) : UniformMassHomBound dimension mass

Cancel a positive degree from the two sides of a uniform mass--Hom estimate. The three mathematical inputs are the base estimate, the adjunction dimension formula, and the HN mass formula.

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.finiteDimensional_of_finiteType_field (k : Type w) (ell : Type w') [Field k] [Field ell] [Algebra k ell] [Algebra.FiniteType k ell] : FiniteDimensional k ell

Zariski's lemma in the exact form used in Theorem 8.23: a finite-type extension of fields is finite-dimensional.

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FieldExtensionAdjunctionDimensionFormula {k : Type w} {ell : Type w'} [Field k] [Field ell] [Algebra k ell] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] {Cell : Type u''} [Category.{v', u''} Cell] [Preadditive Cell] [Linear ell Cell] (push : Functor Cell C) (G : C) (Gell : Cell) : Prop

The adjunction/restriction-of-scalars dimension formula used in (8.4). Its geometric constructor is deliberately left to scalar base change.

Equations

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

def CategoryTheory.Triangulated.StabilityCondition.WithClassMap.FieldExtensionHNMassFormula {k : Type w} {ell : Type w'} [Field k] [Field ell] [Algebra k ell] {C : Type u} [Category.{v, u} C] [Preadditive C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Cell : Type u''} [Category.{v', u''} Cell] [Preadditive Cell] [Limits.HasZeroObject Cell] [HasShift Cell ℤ] [∀ (n : ℤ), (shiftFunctor Cell n).Additive] [Pretriangulated Cell] {Lambda : Type u'} [AddCommGroup Lambda] {LambdaEll : Type u_1} [AddCommGroup LambdaEll] {vC : K₀ C →+ Lambda} {vCell : K₀ Cell →+ LambdaEll} (sigma : WithClassMap C vC) (sigmaEll : WithClassMap Cell vCell) (push : Functor Cell C) : Prop

The HN-preserving pushforward mass formula used in (8.4). This is the mass consequence supplied by the scalar-base-change stability machinery.

Equations

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

theorem CategoryTheory.Triangulated.StabilityCondition.WithClassMap.inequality84 {k : Type w} {ell : Type w'} [Field k] [Field ell] [Algebra k ell] [Algebra.FiniteType k ell] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] [Limits.HasZeroObject C] [HasShift C ℤ] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [SerreFunctor.HomFinite k C] {Cell : Type u''} [Category.{v', u''} Cell] [Preadditive Cell] [Linear ell Cell] [Limits.HasZeroObject Cell] [HasShift Cell ℤ] [∀ (n : ℤ), (shiftFunctor Cell n).Additive] [Pretriangulated Cell] [SerreFunctor.HomFinite ell Cell] {Lambda : Type u'} [AddCommGroup Lambda] {LambdaEll : Type u_1} [AddCommGroup LambdaEll] {vC : K₀ C →+ Lambda} {vCell : K₀ Cell →+ LambdaEll} (sigma : WithClassMap C vC) (sigmaEll : WithClassMap Cell vCell) (push : Functor Cell C) (G : C) (Gell : Cell) (hG : sigma.HasMassHomBoundFor G) (hadjunction : FieldExtensionAdjunctionDimensionFormula push G Gell) (hHNMass : sigma.FieldExtensionHNMassFormula sigmaEll push) : sigmaEll.HasMassHomBoundFor Gell

Inequality (8.4) for one finite-type field extension. The same constant as the base mass--Hom bound works after extension: Zariski's lemma makes the degree positive, and the two named formulas cancel it.