Issues

Express cPair through PeriodDomain.centralCharge, or record why not

chris-dare-dev/derived-alg-geo-lean#1810 · opened

on Oct 1, 2026

SF14.5c: Theorem 22.2, the central charge map on Stab(D/S) is a local homeomorphism (BLMNPS Thm 22.2)

chris-dare-dev/derived-alg-geo-lean#1779 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF14.5b: Deforming a stability condition over S along its central charge (BLMNPS Remark 21.19, Lemma 22.3)

chris-dare-dev/derived-alg-geo-lean#1778 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF14.5a: Bridgeland deformation with the support property is a covering map (BLMNPS Thm 12.11)

chris-dare-dev/derived-alg-geo-lean#1777 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF14.4: The space of stability conditions over S, and the statement of Theorem 22.2 (BLMNPS Def 22.1)

chris-dare-dev/derived-alg-geo-lean#1776 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF14.3: Quot^{≤φ}_S(E) is an algebraic space of finite type, universally closed over S (BLMNPS Lemma 21.21)

chris-dare-dev/derived-alg-geo-lean#1775 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF9.7: M_σ(v, φ) → S satisfies the strong existence part of the valuative criterion (BLMNPS Lemma 21.22)

chris-dare-dev/derived-alg-geo-lean#1774 · opened

on Sep 27, 2026

· SF9 — Moduli of σ-semistable objects (BLMNPS §§9, 21)

SF14.2: Stability conditions over a base, and boundedness and finite type of P_σ(I; v) (BLMNPS Defs 21.13, 21.15, Lemma 21.20)

chris-dare-dev/derived-alg-geo-lean#1773 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF14.1c: Semicontinuity of phases and openness of lying in P(I) for flat families (BLMNPS Lemma 20.9, Prop 20.8, Cor 20.10)

chris-dare-dev/derived-alg-geo-lean#1772 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF14.1b: Flat families of stability conditions over a base (BLMNPS Def 20.5, Lemmas 20.3–20.4)

chris-dare-dev/derived-alg-geo-lean#1771 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF14.1a: Fibrewise collections of stability conditions over a base, with the openness predicates of Def 20.1 (BLMNPS Def 20.1, Remark 21.4)

chris-dare-dev/derived-alg-geo-lean#1770 · opened

on Sep 27, 2026

· SF14 — Stability conditions over a base and Theorem 22.2 (BLMNPS §§20–22)

SF13.5: The G̃L⁺(2,ℝ) action on HN structures over C, and tilting (BLMNPS Remark 13.15, Prop 19.5)

chris-dare-dev/derived-alg-geo-lean#1769 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.4: HN structures over C from HN structures on the fibres (BLMNPS Thm 18.7)

chris-dare-dev/derived-alg-geo-lean#1768 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.3b: C-torsion theories and the support property over C (BLMNPS §§17.2, 18.1)

chris-dare-dev/derived-alg-geo-lean#1767 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.3a: Openness of flatness gives a C-torsion theory (BLMNPS Thm 17.1)

chris-dare-dev/derived-alg-geo-lean#1766 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.2c: The HN property over C: criterion, semistable reduction and noetherianity (BLMNPS Props 13.16, 15.10, 15.14)

chris-dare-dev/derived-alg-geo-lean#1765 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.2b: Hearts with a weak stability function over C are HN structures (BLMNPS Props 13.14, 15.9)

chris-dare-dev/derived-alg-geo-lean#1764 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.2a: Weak stability functions over a Dedekind scheme and their fibres (BLMNPS §15.1, Lemmas 13.11–13.12, 16.2)

chris-dare-dev/derived-alg-geo-lean#1763 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.1: Dedekind schemes and Harder–Narasimhan structures over them (BLMNPS Defs 13.1, 13.3, 15.1)

chris-dare-dev/derived-alg-geo-lean#1762 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.0b: Noetherian torsion subcategories and terminating chains for weak stability functions (BLMNPS Lemmas 14.8, 14.11)

chris-dare-dev/derived-alg-geo-lean#1761 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF13.0a: Finitely many classes under the support property, and local finiteness from support (BLMNPS Remark 12.3)

chris-dare-dev/derived-alg-geo-lean#1760 · opened

on Sep 27, 2026

· SF13 — Harder–Narasimhan structures over a curve, as theorems (BLMNPS Part III)

SF9.8: Research: the route to Θ-reductivity and S-completeness of M_σ(v, φ) (gap F3)

chris-dare-dev/derived-alg-geo-lean#1759 · opened

on Sep 27, 2026

· SF9 — Moduli of σ-semistable objects (BLMNPS §§9, 21)

SF9.6: Extensions of bounded families are bounded (BLMNPS Lemma 9.6, with Lemma 8.9's first part)

chris-dare-dev/derived-alg-geo-lean#1758 · opened

on Sep 27, 2026

· SF9 — Moduli of σ-semistable objects (BLMNPS §§9, 21)

SF9.5: M_pug(𝒟/S) for a semiorthogonal component is cut out of M_pug(X/S) by an open property (BLMNPS Def 9.1, Prop 9.2, Lemma 9.3)

chris-dare-dev/derived-alg-geo-lean#1757 · opened

on Sep 27, 2026

· SF9 — Moduli of σ-semistable objects (BLMNPS §§9, 21)

ART1.5: Artin's criterion, and M_pug is an algebraic stack

chris-dare-dev/derived-alg-geo-lean#1756 · opened

on Sep 27, 2026

· ART1 — Artin's axioms for the moduli of complexes

Navigation Menu

Repository navigation

Issues

Express cPair through PeriodDomain.centralCharge, or record why not

SF14.5c: Theorem 22.2, the central charge map on Stab(D/S) is a local homeomorphism (BLMNPS Thm 22.2)

SF14.5b: Deforming a stability condition over S along its central charge (BLMNPS Remark 21.19, Lemma 22.3)

SF14.5a: Bridgeland deformation with the support property is a covering map (BLMNPS Thm 12.11)

SF14.4: The space of stability conditions over S, and the statement of Theorem 22.2 (BLMNPS Def 22.1)

SF14.3: Quot^{≤φ}_S(E) is an algebraic space of finite type, universally closed over S (BLMNPS Lemma 21.21)

SF9.7: M_σ(v, φ) → S satisfies the strong existence part of the valuative criterion (BLMNPS Lemma 21.22)

SF14.2: Stability conditions over a base, and boundedness and finite type of P_σ(I; v) (BLMNPS Defs 21.13, 21.15, Lemma 21.20)

SF14.1c: Semicontinuity of phases and openness of lying in P(I) for flat families (BLMNPS Lemma 20.9, Prop 20.8, Cor 20.10)

SF14.1b: Flat families of stability conditions over a base (BLMNPS Def 20.5, Lemmas 20.3–20.4)

SF14.1a: Fibrewise collections of stability conditions over a base, with the openness predicates of Def 20.1 (BLMNPS Def 20.1, Remark 21.4)

SF13.5: The G̃L⁺(2,ℝ) action on HN structures over C, and tilting (BLMNPS Remark 13.15, Prop 19.5)

SF13.4: HN structures over C from HN structures on the fibres (BLMNPS Thm 18.7)

SF13.3b: C-torsion theories and the support property over C (BLMNPS §§17.2, 18.1)

SF13.3a: Openness of flatness gives a C-torsion theory (BLMNPS Thm 17.1)

SF13.2c: The HN property over C: criterion, semistable reduction and noetherianity (BLMNPS Props 13.16, 15.10, 15.14)

SF13.2b: Hearts with a weak stability function over C are HN structures (BLMNPS Props 13.14, 15.9)

SF13.2a: Weak stability functions over a Dedekind scheme and their fibres (BLMNPS §15.1, Lemmas 13.11–13.12, 16.2)

SF13.1: Dedekind schemes and Harder–Narasimhan structures over them (BLMNPS Defs 13.1, 13.3, 15.1)

SF13.0b: Noetherian torsion subcategories and terminating chains for weak stability functions (BLMNPS Lemmas 14.8, 14.11)

SF13.0a: Finitely many classes under the support property, and local finiteness from support (BLMNPS Remark 12.3)

SF9.8: Research: the route to Θ-reductivity and S-completeness of M_σ(v, φ) (gap F3)

SF9.6: Extensions of bounded families are bounded (BLMNPS Lemma 9.6, with Lemma 8.9's first part)

SF9.5: M_pug(𝒟/S) for a semiorthogonal component is cut out of M_pug(X/S) by an open property (BLMNPS Def 9.1, Prop 9.2, Lemma 9.3)

ART1.5: Artin's criterion, and M_pug is an algebraic stack