BridgelandStability Comparator Manual

1. Overview🔗

comparator

Repository: https://github.com/mattrobball/BridgelandStability

This manual presents the comparator view of the formalization. It was generated mechanically from the trusted formalization base walk rooted at the comparator target theorem in BridgelandStability.NumericalStabilityManifold. The formalization covers 57 declarations across 11 modules.

1.1. CategoryTheory.Triangulated.NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent🔗

Theorem | BridgelandStability.NumericalStabilityManifold | Source | Open Issue

/-- **Bridgeland's Corollary 1.3** for numerical stability conditions. Each connected component of `Stab_N(D)` is a complex manifold of dimension `rk(N(D))`. This is a specialization of the generic class-map theorem to `v = numericalQuotientMap k C`, which is surjective by definition. -/ @[informal "Corollary 1.3" "complex manifold conclusion only; local homeomorphism is in componentTopologicalLinearLocalModel"] theorem NumericalStabilityCondition.existsComplexManifoldOnConnectedComponent (k : Type w) [Field k] [Linear k C] [IsFiniteType k C] [(shiftFunctor C (1 : ℤ)).Linear k] [NumericallyFinite k C] (cc : StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)) : ∃ (E : Type u) (_ : NormedAddCommGroup E) (_ : NormedSpace ℂ E) (_ : FiniteDimensional ℂ E) (_ : ChartedSpace E (NumericalComponent (k := k) C cc)), IsManifold (𝓘(ℂ, E)) (⊤ : WithTop ℕ∞) (NumericalComponent (k := k) C cc)
Show proof:= C:Type uinst✝¹¹:Category.{v, u} Cinst✝¹⁰:HasZeroObject Cinst✝⁹:HasShift C ℤinst✝⁸:Preadditive Cinst✝⁷:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁶:Pretriangulated Cinst✝⁵:IsTriangulated Ck:Type winst✝⁴:Field kinst✝³:Linear k Cinst✝²:IsFiniteType k Cinst✝¹:Functor.Linear k (shiftFunctor C 1)inst✝:NumericallyFinite k Ccc:StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)⊢ ∃ E x x_1, ∃ (_ : FiniteDimensional ℂ E), ∃ x_3, IsManifold 𝓘(ℂ, E) ⊤ (NumericalComponent k C cc) C:Type uinst✝¹¹:Category.{v, u} Cinst✝¹⁰:HasZeroObject Cinst✝⁹:HasShift C ℤinst✝⁸:Preadditive Cinst✝⁷:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝⁶:Pretriangulated Cinst✝⁵:IsTriangulated Ck:Type winst✝⁴:Field kinst✝³:Linear k Cinst✝²:IsFiniteType k Cinst✝¹:Functor.Linear k (shiftFunctor C 1)inst✝:NumericallyFinite k Ccc:StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)this:Fact (Function.Surjective ⇑(numericalQuotientMap k C))⊢ ∃ E x x_1, ∃ (_ : FiniteDimensional ℂ E), ∃ x_3, IsManifold 𝓘(ℂ, E) ⊤ (NumericalComponent k C cc) All goals completed! 🐙

1.2. Declaration census🔗

Every constant in the transitive closure of the target theorem's type. Auxiliary declarations are resolved to their user-facing parent.

126 raw constants: 56 user-facing, 0 auxiliary.

  • K0Presentation — user

  • CategoryTheory.IsStrict — user

  • CategoryTheory.IsStrictArtinianObject — user

  • CategoryTheory.IsStrictMono — user

  • CategoryTheory.IsStrictNoetherianObject — user

  • CategoryTheory.StrictSubobject — user

  • CategoryTheory.isStrictArtinianObject — user

  • CategoryTheory.isStrictNoetherianObject — user

  • K0Presentation.IsAdditive — user

  • K0Presentation.K0 — user

  • K0Presentation.lift — user

  • K0Presentation.mk — constructor → K0Presentation

  • K0Presentation.obj₁ — projection → K0Presentation

  • K0Presentation.obj₂ — projection → K0Presentation

  • K0Presentation.obj₃ — projection → K0Presentation

  • K0Presentation.subgroup — user

  • CategoryTheory.IsStrictMono.mk — constructor → CategoryTheory.IsStrictMono

  • CategoryTheory.Subobject.IsStrict — user

  • CategoryTheory.Triangulated.HNFiltration — user

  • CategoryTheory.Triangulated.IsFiniteType — user

  • CategoryTheory.Triangulated.IsTriangleAdditive — user

  • CategoryTheory.Triangulated.K₀ — user

  • CategoryTheory.Triangulated.NumericalComponent — user

  • CategoryTheory.Triangulated.NumericalK₀ — user

  • CategoryTheory.Triangulated.NumericallyFinite — user

  • CategoryTheory.Triangulated.PostnikovTower — user

  • CategoryTheory.Triangulated.Slicing — user

  • CategoryTheory.Triangulated.basisNhd — user

  • CategoryTheory.Triangulated.cl — user

  • CategoryTheory.Triangulated.eulerForm — user

  • CategoryTheory.Triangulated.eulerFormInner — user

  • CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive — user

  • CategoryTheory.Triangulated.eulerFormObj — user

  • CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive — user

  • CategoryTheory.Triangulated.eulerFormRad — user

  • CategoryTheory.Triangulated.instIsAdditiveSubtypeTriangleMemSetDistinguishedTrianglesTrianglePresentationOfIsTriangleAdditive — user

  • CategoryTheory.Triangulated.numericalQuotientMap — user

  • CategoryTheory.Triangulated.slicingDist — user

  • CategoryTheory.Triangulated.stabSeminorm — user

  • CategoryTheory.Triangulated.trianglePresentation — user

  • K0Presentation.IsAdditive.mk — constructor → K0Presentation.IsAdditive

  • K0Presentation.instAddCommGroupK0._proof_1 — internal → K0Presentation.instAddCommGroupK0

  • K0Presentation.lift._proof_1 — internal → K0Presentation.lift

  • CategoryTheory.Subobject.IsStrict._proof_1 — internal → CategoryTheory.Subobject.IsStrict

  • CategoryTheory.Subobject.IsStrict._proof_2 — internal → CategoryTheory.Subobject.IsStrict

  • CategoryTheory.Subobject.IsStrict._proof_3 — internal → CategoryTheory.Subobject.IsStrict

  • CategoryTheory.Subobject.IsStrict._proof_4 — internal → CategoryTheory.Subobject.IsStrict

  • CategoryTheory.Triangulated.HNFiltration.exists_nonzero_first — user

  • CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last — user

  • CategoryTheory.Triangulated.HNFiltration.mk — constructor → CategoryTheory.Triangulated.HNFiltration

  • CategoryTheory.Triangulated.HNFiltration.toPostnikovTower — projection → CategoryTheory.Triangulated.HNFiltration

  • CategoryTheory.Triangulated.HNFiltration.φ — projection → CategoryTheory.Triangulated.HNFiltration

  • CategoryTheory.Triangulated.IsFiniteType.mk — constructor → CategoryTheory.Triangulated.IsFiniteType

  • CategoryTheory.Triangulated.IsTriangleAdditive.mk — constructor → CategoryTheory.Triangulated.IsTriangleAdditive

  • CategoryTheory.Triangulated.K₀.instAddCommGroup — user

  • CategoryTheory.Triangulated.K₀.lift — user

  • CategoryTheory.Triangulated.K₀.of — user

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup — user

  • CategoryTheory.Triangulated.NumericallyFinite.mk — constructor → CategoryTheory.Triangulated.NumericallyFinite

  • CategoryTheory.Triangulated.PostnikovTower._proof_1 — internal → CategoryTheory.Triangulated.PostnikovTower

  • CategoryTheory.Triangulated.PostnikovTower._proof_3 — internal → CategoryTheory.Triangulated.PostnikovTower

  • CategoryTheory.Triangulated.PostnikovTower.factor — user

  • CategoryTheory.Triangulated.PostnikovTower.mk — constructor → CategoryTheory.Triangulated.PostnikovTower

  • CategoryTheory.Triangulated.PostnikovTower.n — projection → CategoryTheory.Triangulated.PostnikovTower

  • CategoryTheory.Triangulated.PostnikovTower.triangle — projection → CategoryTheory.Triangulated.PostnikovTower

  • CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap — user

  • CategoryTheory.Triangulated.Slicing.IntervalCat — user

  • CategoryTheory.Triangulated.Slicing.IsLocallyFinite — user

  • CategoryTheory.Triangulated.Slicing.P — projection → CategoryTheory.Triangulated.Slicing

  • CategoryTheory.Triangulated.Slicing.intervalCat_hasCokernels — user

  • CategoryTheory.Triangulated.Slicing.intervalCat_hasKernels — user

  • CategoryTheory.Triangulated.Slicing.intervalProp — user

  • CategoryTheory.Triangulated.Slicing.mk — constructor → CategoryTheory.Triangulated.Slicing

  • CategoryTheory.Triangulated.Slicing.phiMinus — user

  • CategoryTheory.Triangulated.Slicing.phiPlus — user

  • CategoryTheory.Triangulated.StabilityCondition.WithClassMap — user

  • CategoryTheory.Triangulated.numericalQuotientMap._proof_1 — internal → CategoryTheory.Triangulated.numericalQuotientMap

  • CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last._proof_1 — internal → CategoryTheory.Triangulated.HNFiltration.exists_nonzero_last

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_1 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_12 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_14 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_17 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_4 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._aux_8 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_10 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_11 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_16 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_19 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_20 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_21 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_22 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_23 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_3 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_6 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.K₀.instAddCommGroup._proof_7 — internal → CategoryTheory.Triangulated.K₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_1 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_12 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_14 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_17 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_4 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._aux_8 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_10 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_11 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_16 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_19 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_20 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_21 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_22 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_23 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_3 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_6 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup._proof_7 — internal → CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup

  • CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.Z — projection → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap

  • CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.charge — user

  • CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.mk — constructor → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap

  • CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap.slicing — projection → CategoryTheory.Triangulated.PreStabilityCondition.WithClassMap

  • CategoryTheory.Triangulated.Slicing.IsLocallyFinite.mk — constructor → CategoryTheory.Triangulated.Slicing.IsLocallyFinite

  • CategoryTheory.Triangulated.Slicing.phiMinus._proof_1 — internal → CategoryTheory.Triangulated.Slicing.phiMinus

  • CategoryTheory.Triangulated.Slicing.phiMinus._proof_2 — internal → CategoryTheory.Triangulated.Slicing.phiMinus

  • CategoryTheory.Triangulated.Slicing.phiPlus._proof_1 — internal → CategoryTheory.Triangulated.Slicing.phiPlus

  • CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component — user

  • CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex — user

  • CategoryTheory.Triangulated.StabilityCondition.WithClassMap.mk — constructor → CategoryTheory.Triangulated.StabilityCondition.WithClassMap

  • CategoryTheory.Triangulated.StabilityCondition.WithClassMap.toWithClassMap — projection → CategoryTheory.Triangulated.StabilityCondition.WithClassMap

  • CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace — user

  • CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace._proof_1 — internal → CategoryTheory.Triangulated.StabilityCondition.WithClassMap.topologicalSpace

1.3. Dependency graph🔗

Click a node to navigate to its declaration.