Transporting weak slope data along an equivalence of abelian categories

WeakSlopeData A is two homomorphisms out of K₀Ab A together with two sign conditions, so an equivalence e : A ≌ B carries it to WeakSlopeData B by precomposing with K₀Ab.congr e. This file does that and records what the transported rank, degree, slope and charge are.

Why it is needed

Numerical data is written on the category the objects live in. The stability machinery is written on the heart of a t-structure. Algebra/Homology/DerivedCategory/Heart.lean identifies the two for the canonical t-structure, and this file is what lets a slope defined on the first be read on the second — the concrete case being the μ-slope of the Gieseker lane, which is defined on coherent sheaves while the Mukai tilt assembly wants it on a heart.

The direction to keep straight

congr transports along e, so the transported data on B evaluates an object by pulling it back through e.inverse. Both readings are recorded: congr_rank is the one that holds by definition, and congr_rank_functor is the one a consumer starting from an object of A wants. Nothing is transported by rfl alone — congr_rank_functor needs the unit isomorphism, which is why it is a theorem and not a simp unfolding.

Semistability

Semistability is not a statement about a homomorphism: it quantifies over the subobjects of an object. It transports because Subobject.mapEquivalence is an order isomorphism and in particular surjective, so every subobject of the image is the image of a subobject, and its slope is the original slope by mapFunctorIso.

What is not here

The Harder–Narasimhan property itself. A filtration also names the cokernel of each chain step, so transporting one needs Subobject.cokernelOfLEMapFunctorIso and an isomorphism-invariance lemma for filtrations that does not yet exist.

theorem CategoryTheory.Triangulated.not_isZero_inverse_obj {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) {E : B} (hE : ¬Limits.IsZero E) : ¬Limits.IsZero (e.inverse.obj E)

An equivalence reflects nonzero objects: the inverse of a nonzero object is nonzero.

noncomputable def CategoryTheory.Triangulated.WeakSlopeData.congr {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) : WeakSlopeData B

Weak slope data transported along an equivalence.

Both homomorphisms are precomposed with K₀Ab.congr e run backwards, so the transported data reads an object of B by pulling it back to A. The two sign conditions transport because the pullback of a nonzero object is nonzero.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_rank {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (E : B) : (D.congr e).rank E = D.rank (e.inverse.obj E)

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_degree {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (E : B) : (D.congr e).degree E = D.degree (e.inverse.obj E)

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_symm_of_functor {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) (X : A) : (K₀Ab.congr e).symm (K₀Ab.of (e.functor.obj X)) = K₀Ab.of X

The Grothendieck class of a transported object is the original class. Everything below is this one equation read through a different homomorphism.

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_rank_functor {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (X : A) : (D.congr e).rank (e.functor.obj X) = D.rank X

The reading a consumer starting from an object of A wants. It is the unit isomorphism, not rfl. It is deliberately not a simp lemma: congr_rank already rewrites the left-hand side to the e.inverse form, so both cannot fire.

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_degree_functor {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (X : A) : (D.congr e).degree (e.functor.obj X) = D.degree X

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_charge {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (E : B) : (D.congr e).charge E = D.charge (e.inverse.obj E)

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_charge_functor {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (X : A) : (D.congr e).charge (e.functor.obj X) = D.charge X

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_slope {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (E : B) : (D.congr e).slope E = D.slope (e.inverse.obj E)

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_slope_functor {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (X : A) : (D.congr e).slope (e.functor.obj X) = D.slope X

@[simp]

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_topSlope {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (E : B) : (D.congr e).topSlope E = D.topSlope (e.inverse.obj E)

The honest slope transports too. The two cases are rank zero, where both sides are ⊤, and positive rank, where both sides are the coerced ratio.

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_topSlope_functor {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) (X : A) : (D.congr e).topSlope (e.functor.obj X) = D.topSlope X

theorem CategoryTheory.Triangulated.WeakSlopeData.not_isZero_functor_obj {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (e : A ≌ B) {Z : A} (hZ : ¬Limits.IsZero Z) : ¬Limits.IsZero (e.functor.obj Z)

An equivalence carries nonzero objects to nonzero objects.

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_topSlope_mapFunctor {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) {Z : A} (P : Subobject Z) [e.functor.PreservesMonomorphisms] : (D.congr e).topSlope (Subobject.underlying.obj (Subobject.mapFunctor e.functor P)) = D.topSlope (Subobject.underlying.obj P)

The slope of a transported subobject is the original slope.

theorem CategoryTheory.Triangulated.WeakSlopeData.congr_isSemistable {A : Type u₁} [Category.{v₁, u₁} A] [Abelian A] {B : Type u₂} [Category.{v₂, u₂} B] [Abelian B] (D : WeakSlopeData A) (e : A ≌ B) [e.functor.PreservesMonomorphisms] [e.inverse.PreservesMonomorphisms] {Z : A} (h : D.toWeakStabilityFunction.IsSemistable Z) : (D.congr e).toWeakStabilityFunction.IsSemistable (e.functor.obj Z)

Semistability transports along an equivalence.

Every subobject of the image is the image of a subobject, because Subobject.mapEquivalence is an order isomorphism and so surjective; its slope is the original slope.