Pullback and cokernel transport in an owner thin interval #
Strict subobjects of a strict quotient pull back to strict subobjects. Their cokernels agree up to isomorphism, so the perturbed charge and phase transport across the pullback square. These are the categorical and phase-theoretic inputs for strict maximal destabilizing quotient selection.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.bot_arrow_strictMono
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C s a b}
:
The bottom subobject has a strict canonical arrow.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.pullbackProjection_strictEpi
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X Y : Slicing.IntervalCat C s a b}
(p : X ⟶ Y)
(hp : IsStrictEpi p)
(B : Subobject Y)
:
Pulling back a strict epimorphism along an interval subobject preserves strict epimorphy of the pullback projection.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.strictShortExact_of_kernel_strictEpi
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
(S : ShortComplex (Slicing.IntervalCat C s a b))
(hKer : Limits.IsLimit (Limits.KernelFork.ofι S.f ⋯))
(hg : IsStrictEpi S.g)
:
A kernel followed by a strict epimorphism is an owner strict short exact sequence in a thin interval.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.strictShortExact_pullback_left
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{K E Q : Slicing.IntervalCat C s a b}
{i : K ⟶ E}
{q : E ⟶ Q}
(hiq : CategoryStruct.comp i q = 0)
(hKer : Limits.IsLimit (Limits.KernelFork.ofι i hiq))
(hq : IsStrictEpi q)
(B : Subobject Q)
:
let pb := (Subobject.pullback q).obj B;
let m :=
have hiB := ⋯;
pb.factorThru i ⋯;
StrictShortExact
{ X₁ := K, X₂ := Subobject.underlying.obj pb, X₃ := Subobject.underlying.obj B, f := m, g := Subobject.pullbackπ q B,
zero := ⋯ }
Pulling a kernel--strict-epimorphism sequence back along an interval subobject preserves owner strict short exactness.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.strictShortExact_pullback_right
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{E Q Y : Slicing.IntervalCat C s a b}
(q : E ⟶ Q)
(hq : IsStrictEpi q)
(B : Subobject Q)
(g : Q ⟶ Y)
(hBg : CategoryStruct.comp B.arrow g = 0)
(hBKer : Limits.IsLimit (Limits.KernelFork.ofι B.arrow hBg))
(hg : IsStrictEpi g)
:
let pb := (Subobject.pullback q).obj B;
let p := CategoryStruct.comp q g;
StrictShortExact { X₁ := Subobject.underlying.obj pb, X₂ := E, X₃ := Y, f := pb.arrow, g := p, zero := ⋯ }
The complementary pullback sequence associated to two composable strict epimorphisms is owner strict short exact.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.pullbackArrow_strictMono
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X Y : Slicing.IntervalCat C s a b}
(p : X ⟶ Y)
(B : Subobject Y)
(hB : IsStrictMono B.arrow)
:
IsStrictMono ((Subobject.pullback p).obj B).arrow
Pulling back a strict interval subobject preserves strictness of its canonical arrow.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.le_pullbackCokernel
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
(B : Subobject (Limits.cokernel M.arrow))
:
A kernel subobject lies below the pullback of every subobject of its canonical cokernel.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.ofLE_pullbackProjection_eq_zero
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
(B : Subobject (Limits.cokernel M.arrow))
:
CategoryStruct.comp (M.ofLE ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B) ⋯)
(Subobject.pullbackπ (Limits.cokernel.π M.arrow) B) = 0
The inclusion of a kernel subobject into a cokernel pullback is killed by the pullback projection.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.lt_pullbackCokernel_of_ne_bot
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C s a b}
{M : Subobject X}
{B : Subobject (Limits.cokernel M.arrow)}
(hB : B ≠ ⊥)
:
A nonzero subobject of a cokernel pulls back to a strict enlargement of the kernel subobject.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.pullbackCokernel_ne_top
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C s a b}
{M : Subobject X}
{B : Subobject (Limits.cokernel M.arrow)}
(hB : B ≠ ⊤)
(hBstrict : IsStrictMono B.arrow)
:
A strict proper subobject of a cokernel cannot pull back to the top subobject.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.cokernel_not_isZero_of_ne_top
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C s a b}
{M : Subobject X}
(hM : M ≠ ⊤)
(hMstrict : IsStrictMono M.arrow)
:
A strict proper subobject has a nonzero cokernel.
noncomputable def
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.Slicing.IntervalCat.cokernelPullbackIso
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{s : Slicing C}
{a b : ℝ}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C s a b}
(M : Subobject X)
{B : Subobject (Limits.cokernel M.arrow)}
(hB : IsStrictMono B.arrow)
:
Pulling back a strict subobject along a cokernel projection preserves its cokernel object up to canonical isomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.charge_cokernelPullback
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
{σ : StabilityCondition.WithClassMap C κ}
{a b : ℝ}
{F : SkewedStabilityFunction C κ σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(M : Subobject X)
{B : Subobject (Limits.cokernel M.arrow)}
(hB : IsStrictMono B.arrow)
:
F.charge (Limits.cokernel ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B).arrow).obj = F.charge (Limits.cokernel B.arrow).obj
The perturbed charge of the cokernel is invariant under pullback along a cokernel projection.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase_cokernelPullback
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
{σ : StabilityCondition.WithClassMap C κ}
{a b : ℝ}
{F : SkewedStabilityFunction C κ σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{X : Slicing.IntervalCat C σ.slicing a b}
(M : Subobject X)
{B : Subobject (Limits.cokernel M.arrow)}
(hB : IsStrictMono B.arrow)
:
F.phase (Limits.cokernel ((Subobject.pullback (Limits.cokernel.π M.arrow)).obj B).arrow).obj = F.phase (Limits.cokernel B.arrow).obj
The perturbed phase of the cokernel is invariant under pullback along a cokernel projection.
theorem
CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Deformation.SkewedStabilityFunction.phase_cokernel_lt_of_phase_gt_strictSubobject
(C : Type u)
[Category.{v, u} C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[IsTriangulated C]
{Λ : Type u'}
[AddCommGroup Λ]
{κ : K₀ C →+ Λ}
{σ : StabilityCondition.WithClassMap C κ}
{a b : ℝ}
{F : SkewedStabilityFunction C κ σ.slicing a b}
[Fact (a < b)]
[Fact (b - a ≤ 1)]
{Y : Slicing.IntervalCat C σ.slicing a b}
{A : Subobject Y}
(hAne : A ≠ ⊥)
(hAtop : A ≠ ⊤)
(hAstrict : IsStrictMono A.arrow)
(hAphase : F.phase Y.obj < F.phase (Subobject.underlying.obj A).obj)
(hCharge : ∀ {E : C}, Slicing.intervalProp C σ.slicing a b E → ¬Limits.IsZero E → F.ChargeNe E)
{L U : ℝ}
(hWindow : ∀ (Z : Slicing.IntervalCat C σ.slicing a b), ¬Limits.IsZero Z.obj → L < F.phase Z.obj ∧ F.phase Z.obj < U)
(hWidth : U - L < 1)
:
In a common phase window of width less than one, the cokernel of an above-phase proper strict subobject has phase strictly below the original object.