Spherical signed-ray loci in the exp(β + iω) chart

For a real vector space V with a symmetric bilinear form q — standing for NS(X) ⊗ ℝ with the intersection form — the vector

℧ = exp(β + iω) = (1, β + iω, (β + iω)²/2)

pairs against a class δ = (r, Δ, s) of the real Mukai extension ℝ ⊕ V ⊕ ℝ. This file computes that pairing and names the locus

H(δ) = { (β, ω) : (℧, δ) ∈ ℝ_{≤0} }

together with the complement of the union of these loci over classes with ⟪δ, δ⟫ = -2 and positive rank.

What this is a theorem about, and what it is not

Everything here is arithmetic in a real vector space carrying a symmetric bilinear form. There is no K3 surface: no Néron–Severi group, no ample cone, no Hodge index theorem, no Mukai vector of an object, no stability condition and no Stab(X). Mukai.RealExtension V is a triple, not N(X) ⊗ ℝ, and signedRayRegularLocus is not claimed to be the image of anything under a map from a space of stability conditions.

In particular the Hodge index theorem is not used and not assumed. Where the geometric theory would invoke it — to say that q is negative definite on ω^⊥ — the statements that need it carry it as an explicit hypothesis, and none of the statements in this file needs it. That is why this file stops where it does: the local-finiteness theorem, which is the first statement that genuinely consumes negative-definiteness and lattice discreteness, is deliberately left to a follow-up rather than stated here with hypotheses nothing here can discharge.

This is the same discipline Walls/Numerical/Basic.lean applies to tilt walls and LinearAlgebra/Lattice/Mukai/Basic.lean applies to the integral Mukai extension.

Not the same loci as Walls/Numerical

Walls/Numerical/Basic.lean is the tilt-stability wall structure: a numerical class is a triple of reals (ch₀, ch₁·H, ch₂), the parameter space is the (s, t) half plane, and the walls are nested conics. This file is a different numerical locus: the parameter space is a pair (β, ω) of vectors, the index set is the spherical classes, and nonpositiveRayLocus is a real half-space rather than a circle. The two files share no declaration and neither imports the other. Do not merge them.

The real extension is a twin of Mukai.pairing, not a generalisation

Mukai.pairing is ℤ-valued on ℤ × N × ℤ for b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ. The chart lives over ℝ, so the formulas below are restated rather than reused. Generalising Mukai/Basic.lean over a base ring would be the tidier fix and is deliberately not done here: it would rewrite three merged modules and their audit records for a file that does not yet need the generality.

The two are connected by IntegralComparison, which supplies the missing datum — an additive map N →+ V carrying b to q — and by isSpherical_map_iff, which says the two sphericity conditions agree across it. Nothing here constructs an IntegralComparison; producing one is the geometric obligation of exhibiting NS(X) with its intersection form, and Mukai/Basic.lean says the same thing about its own identification.

Main results

• two_mul_rk_mul_pairingRe — the identity. 2r·Re(℧,δ) collapses to ⟪δ,δ⟫ + r²·q(ω,ω) − q(Δ − rβ, Δ − rβ), with no side condition. Bridgeland's formula (⋆) is this divided by 2r, and is therefore conditional on r ≠ 0 in a way the undivided form is not.
• pairingIm_eq_of_symm — Im(℧,δ) = q(Δ − rβ, ω). This is the statement that a signed-ray locus meets the real axis exactly on ω^⊥.
• mem_nonpositiveRayLocus_iff_of_isSpherical — membership of H(δ) for spherical δ of positive rank, in the form q(Δ − rβ, ω) = 0 ∧ r²·q(ω,ω) ≤ 2 + q(Δ − rβ, Δ − rβ). This is the shape the local-finiteness argument consumes.
• corank_eq_of_isSpherical — the third coordinate of a spherical class is determined by the other two once r ≠ 0.
• pairingRe_of_rk_eq_zero — at rank zero the identity degenerates to 0 = 0 and the real part is the affine expression q(β,Δ) − s. This is the reason the index set is Δ⁺ rather than Δ, recorded rather than left to inference.

The real Mukai extension

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairing {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (v w : Mukai.RealExtension V) : ℝ

The Mukai pairing over ℝ, built from a bilinear form q on the middle summand.

This file used to declare the type and this pairing a second time, as RealMukai and pairing: the same ℝ × V × ℝ, the same q c c' - r*s' - r'*s, the same [AddCommGroup V] [Module ℝ V] and the same bilinear form as Mukai.RealExtension and Mukai.realPairing. The two docstrings named each other instead of one importing the other. They are now one, and what is local to this file is the signed-ray-locus arithmetic below.

Note Mukai.realForm is half the self-pairing, so sphericality below reads selfPairing q δ = -2 rather than realForm q δ = -2.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairing q v w = Mukai.realPairing q v w

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairing_mk {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (r : ℝ) (c : V) (s r' : ℝ) (c' : V) (s' : ℝ) : pairing q (r, c, s) (r', c', s') = (q c) c' - r * s' - r' * s

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.selfPairing {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (v : Mukai.RealExtension V) : ℝ

⟪v, v⟫.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.selfPairing_eq_pairing {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (v : Mukai.RealExtension V) : selfPairing q v = pairing q v v

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.selfPairing_mk {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (r : ℝ) (c : V) (s : ℝ) : selfPairing q (r, c, s) = (q c) c - 2 * (r * s)

The chart

exp(β + iω) = (1, β + iω, (β + iω)²/2), split into real and imaginary parts. Squaring gives (β + iω)² = q(β,β) − q(ω,ω) + 2i·q(β,ω), so the halves are as below. Both are elements of Mukai.RealExtension V; the pairing against a real class is computed componentwise because the Mukai form is extended ℂ-bilinearly.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.chartRe {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : Mukai.RealExtension V

The real part of exp(β + iω).

This is Mukai.expRe, not a second definition of it. This file used to declare the exponential chart a second time, exactly as it used to declare the pairing a second time — the same (1, β, (q β β - q ω ω)/2), in a file that already imports Mukai/RealForm.lean. The names are kept because the nonpositiveRayLocus statements below read better with them, but they are abbreviations now, so the (β, ω) chart of this subtree and the exponential chart of the period-domain subtree are one object rather than two.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.chartRe q β ω = Mukai.expRe q β ω

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.chartIm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : Mukai.RealExtension V

The imaginary part of exp(β + iω). As with chartRe, this is Mukai.expIm and not a second definition.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.chartIm q β ω = Mukai.expIm q β ω

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.chartRe_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : chartRe q β ω = (1, β, ((q β) β - (q ω) ω) / 2)

The chart in coordinates. Not a simp lemma: chartRe is an abbreviation for Mukai.expRe, so tagging this would unfold the exponential chart globally and displace the normal form the period-domain layer already uses — Mukai.realPairing_expRe_expRe and its siblings would become redundant. The two proofs below name it explicitly instead.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.chartIm_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : chartIm q β ω = (0, ω, (q β) ω)

The imaginary part in coordinates. Not a simp lemma, for the reason given at chartRe_eq.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairingRe {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (δ : Mukai.RealExtension V) : ℝ

Re (℧, δ) for ℧ = exp(β + iω). Inherits noncomputable from chartRe.

Equations

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

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairingIm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (δ : Mukai.RealExtension V) : ℝ

Im (℧, δ) for ℧ = exp(β + iω).

noncomputable since Mukai.expIm is; the marker is bookkeeping, not mathematics, and it is the price of the two charts being one object.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairingRe_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (δ : Mukai.RealExtension V) : pairingRe q β ω δ = (q β) δ.2.1 - δ.2.2 - δ.1 * (((q β) β - (q ω) ω) / 2)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairingIm_eq {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (δ : Mukai.RealExtension V) : pairingIm q β ω δ = (q ω) δ.2.1 - δ.1 * (q β) ω

The two identities

pairingIm_eq_of_symm and two_mul_rk_mul_pairingRe are the whole computational content of the file. Both need symmetry of q; nothing above this point does.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairingIm_eq_of_symm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hq : ∀ (x y : V), (q x) y = (q y) x) (β ω : V) (δ : Mukai.RealExtension V) : pairingIm q β ω δ = (q (δ.2.1 - δ.1 • β)) ω

The imaginary part is q(Δ − rβ, ω). So (℧, δ) is real exactly when Δ − rβ is q-orthogonal to ω.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.two_mul_rk_mul_pairingRe {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hq : ∀ (x y : V), (q x) y = (q y) x) (β ω : V) (δ : Mukai.RealExtension V) : 2 * δ.1 * pairingRe q β ω δ = selfPairing q δ + δ.1 ^ 2 * (q ω) ω - (q (δ.2.1 - δ.1 • β)) (δ.2.1 - δ.1 • β)

The identity. 2r·Re(℧, δ) collapses to ⟪δ, δ⟫ + r²·q(ω,ω) − q(Δ − rβ, Δ − rβ).

Stated multiplied through by 2r, so it holds for every r, including r = 0, with no side condition. Bridgeland's (⋆) is this divided by 2r; see pairingRe_eq_of_rk_ne_zero for that form and pairingRe_of_rk_eq_zero for what the identity does — and does not — say at rank zero.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairingRe_eq_of_rk_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hq : ∀ (x y : V), (q x) y = (q y) x) (β ω : V) {δ : Mukai.RealExtension V} (hr : δ.1 ≠ 0) : pairingRe q β ω δ = (selfPairing q δ + δ.1 ^ 2 * (q ω) ω - (q (δ.2.1 - δ.1 • β)) (δ.2.1 - δ.1 • β)) / (2 * δ.1)

Bridgeland's (⋆): the divided form, valid only for r ≠ 0.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.two_mul_rk_mul_pairingRe_of_rk_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hq : ∀ (x y : V), (q x) y = (q y) x) (β ω : V) {δ : Mukai.RealExtension V} (hr : δ.1 = 0) : 2 * δ.1 * pairingRe q β ω δ = 0 ∧ selfPairing q δ + δ.1 ^ 2 * (q ω) ω - (q (δ.2.1 - δ.1 • β)) (δ.2.1 - δ.1 • β) = 0

At rank zero the identity carries no information: both sides vanish identically.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairingRe_of_rk_eq_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) {δ : Mukai.RealExtension V} (hr : δ.1 = 0) : pairingRe q β ω δ = (q β) δ.2.1 - δ.2.2

What the real part actually is at rank zero: an affine expression in β, with no quadratic term and no dependence on ω at all.

This is why the index set of walls is Δ⁺ — spherical classes of positive rank — rather than all of Δ. A rank-zero class still cuts out a locus, but the quadric picture that two_mul_rk_mul_pairingRe describes degenerates, and the sphericity hypothesis ⟪δ,δ⟫ = -2 reads q Δ Δ = -2 with s unconstrained.

Spherical classes

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.IsSpherical {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (δ : Mukai.RealExtension V) : Prop

⟪δ, δ⟫ = -2, over ℝ. The real-coefficient twin of Mukai.IsSpherical; isSpherical_map_iff below identifies the two.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.isSpherical_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (δ : Mukai.RealExtension V) : IsSpherical q δ ↔ selfPairing q δ = -2

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.sphericalPlus {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) : Set (Mukai.RealExtension V)

Δ⁺: the spherical classes of positive rank.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.mem_sphericalPlus_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (δ : Mukai.RealExtension V) : δ ∈ sphericalPlus q ↔ IsSpherical q δ ∧ 0 < δ.1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.isSpherical_of_mem_sphericalPlus {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) {δ : Mukai.RealExtension V} (h : δ ∈ sphericalPlus q) : IsSpherical q δ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.rk_pos_of_mem_sphericalPlus {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) {δ : Mukai.RealExtension V} (h : δ ∈ sphericalPlus q) : 0 < δ.1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.corank_eq_of_isSpherical {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) {δ : Mukai.RealExtension V} (hs : IsSpherical q δ) (hr : δ.1 ≠ 0) : δ.2.2 = ((q δ.2.1) δ.2.1 + 2) / (2 * δ.1)

The third coordinate of a spherical class is determined by the other two, once the rank is nonzero.

So a finiteness statement about spherical classes needs no separate control on s: bounding (r, Δ) bounds δ.

The signed-ray loci, and the regular locus they cut out

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.nonpositiveRayLocus {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (δ : Mukai.RealExtension V) : Set (V × V)

H(δ) in the (β, ω) chart: the locus where (℧, δ) is real and non-positive.

Defined for every δ, not only for spherical ones of positive rank — the sphericity and rank hypotheses belong to the theorems, not to the definition.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.mem_nonpositiveRayLocus_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (δ : Mukai.RealExtension V) (p : V × V) : p ∈ nonpositiveRayLocus q δ ↔ pairingIm q p.1 p.2 δ = 0 ∧ pairingRe q p.1 p.2 δ ≤ 0

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.signedRayRegularLocus {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (S : Set (Mukai.RealExtension V)) : Set (V × V)

The signedRayRegularLocus cut out by a set S of classes: the points of the chart on no nonpositiveRayLocus of S. Bridgeland's L(X) is signedRayRegularLocus q (sphericalPlus q).

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.mem_signedRayRegularLocus_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (S : Set (Mukai.RealExtension V)) (p : V × V) : p ∈ signedRayRegularLocus q S ↔ ∀ δ ∈ S, p ∉ nonpositiveRayLocus q δ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.signedRayRegularLocus_antitone {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) {S T : Set (Mukai.RealExtension V)} (h : S ⊆ T) : signedRayRegularLocus q T ⊆ signedRayRegularLocus q S

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.signedRayRegularLocus_eq_compl_iUnion {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (S : Set (Mukai.RealExtension V)) : signedRayRegularLocus q S = (⋃ δ ∈ S, nonpositiveRayLocus q δ)ᶜ

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.mem_nonpositiveRayLocus_iff_of_isSpherical {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (hq : ∀ (x y : V), (q x) y = (q y) x) {δ : Mukai.RealExtension V} (hs : IsSpherical q δ) (hr : 0 < δ.1) (p : V × V) : p ∈ nonpositiveRayLocus q δ ↔ (q (δ.2.1 - δ.1 • p.1)) p.2 = 0 ∧ δ.1 ^ 2 * (q p.2) p.2 ≤ 2 + (q (δ.2.1 - δ.1 • p.1)) (δ.2.1 - δ.1 • p.1)

Membership of a spherical signed-ray locus, in the form the finiteness argument consumes.

The first conjunct puts Δ − rβ in ω^⊥; the second is the inequality that, together with negative-definiteness of q on ω^⊥ and a positive lower bound on q(ω,ω), bounds r and then Δ. Neither of those two extra hypotheses appears here, because neither is needed for the equivalence itself.

The bridge to the integral Mukai extension

Mukai/Basic.lean builds ℤ × N × ℤ with an integral form; this file builds ℝ × V × ℝ with a real one. IntegralComparison is the datum that relates them, and it is supplied, never constructed — producing one is the geometric obligation of exhibiting NS(X) with its intersection form.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.IntegralComparison {V : Type u_1} [AddCommGroup V] [Module ℝ V] (q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) {N : Type u_2} [AddCommGroup N] (b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ) : Type (max u_1 u_2)

An additive map from the middle summand of the integral extension to the middle summand of the real one, carrying b to q.

compat is where the content is; it is stated on all of N, so unlike IntegralMukaiData.b_spec this is a genuine comparison of forms and not a constraint on the image of a single map.

• toFun : N →+ V

  The map on middle summands.

• compat (x y : N) : (q (self.toFun x)) (self.toFun y) = ↑((b x) y)

  The forms agree across it.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.IntegralComparison.map {V : Type u_1} [AddCommGroup V] [Module ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {N : Type u_2} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} (c : IntegralComparison q b) (v : Mukai.MukaiLattice N) : Mukai.RealExtension V

The induced map on Mukai extensions.

Equations

• c.map v = (↑v.1, c.toFun v.2.1, ↑v.2.2)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.IntegralComparison.map_fst {V : Type u_1} [AddCommGroup V] [Module ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {N : Type u_2} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} (c : IntegralComparison q b) (v : Mukai.MukaiLattice N) : (c.map v).1 = ↑v.1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.pairing_map {V : Type u_1} [AddCommGroup V] [Module ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {N : Type u_2} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} (c : IntegralComparison q b) (v w : Mukai.MukaiLattice N) : pairing q (c.map v) (c.map w) = ↑(Mukai.pairing b v w)

The comparison is an isometry onto its image: the real pairing of two mapped classes is the integral pairing, cast.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.selfPairing_map {V : Type u_1} [AddCommGroup V] [Module ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {N : Type u_2} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} (c : IntegralComparison q b) (v : Mukai.MukaiLattice N) : selfPairing q (c.map v) = ↑(Mukai.selfPairing b v)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Spherical.isSpherical_map_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] {q : V →ₗ[ℝ] V →ₗ[ℝ] ℝ} {N : Type u_2} [AddCommGroup N] {b : N →ₗ[ℤ] N →ₗ[ℤ] ℤ} (c : IntegralComparison q b) (v : Mukai.MukaiLattice N) : IsSpherical q (c.map v) ↔ Mukai.IsSpherical b v

The two sphericity conditions agree.