Positive frames, their underlying planes, and the sign that models P⁺

Bridgeland's period domain is not P but one connected component of it, P⁺ — the one containing exp(iω) for an ample class. A component is picked out by an orientation of the positive plane, and PeriodDomain.positivePlanes is a set of submodules, which carries none: Re Ω and Im Ω are an ordered pair and the plane forgets the order.

This file keeps the order. A positive frame is an ordered pair spanning a positive plane. The map framePlane forgets its ordered basis, and forgetPositiveFrame is the corresponding map between the two locus subtypes. The invariant separating the two oriented halves is the sign of a 2 × 2 determinant of pairings against a reference frame.

Why the determinant cannot vanish, and where that comes from

For positive planes W and W₀, orthogonal projection W → W₀ is an isomorphism: its kernel is W ∩ W₀ᗮ, and a nonzero vector there would have Q v > 0 because it lies in W and Q v < 0 because W₀ᗮ is negative definite. That is neg_of_mem_orthogonal, and pairingDet_ne_zero is exactly this argument written in coordinates, which avoids projections and determinants of linear maps entirely.

"Component" is modeled here, not proved

Two things are not claimed, and a definition that quietly assumed either would be wrong:

• That there are exactly two connected components. That needs connectedness of the Grassmannian of positive planes — topology, not lattice theory. What is proved is that the sign invariant splits the positive frames into two nonempty disjoint halves; whether each half is connected is not addressed.
• That the positive half is Bridgeland's. Selecting the component containing exp(iω) = (1, iω, -ω²/2) needs the Mukai extension's own vectors and an ample class, so it needs the bridge from Mukai.MukaiLattice to a bundled form that is out of scope here as it was in the period-domain file. Relative to a reference frame, "positive half" means only what its definition says.

Reference-independence of the partition — that changing the reference either preserves every sign or flips every sign — is not proved here, but it is proved: it is the cocycle of QuadraticForm/PositiveFrameOrientation.lean, which imports this file.

def PeriodDomain.framePlane {M : Type u_1} [AddCommGroup M] [Module ℝ M] (p : M × M) : Submodule ℝ M

Forget the ordered basis of a frame and retain only the plane it spans.

Equations

• PeriodDomain.framePlane p = PeriodDomain.pairSpan p.1 p.2

theorem PeriodDomain.framePlane_mk {M : Type u_1} [AddCommGroup M] [Module ℝ M] (x y : M) : framePlane (x, y) = pairSpan x y

framePlane on an explicit pair is the span of its two entries. The frame-to-plane map is a genuine definition, so consumers that reason about the spanning set need this to reach pairSpan. It is deliberately not @[simp]: rewriting the carrier of a frame's subtype blocks Submodule.mk_eq_zero on elements of that subtype.

def PeriodDomain.IsPositiveFrame {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x y : M) : Prop

An ordered positive frame: an ordered pair spanning a positive plane.

Equations

• PeriodDomain.IsPositiveFrame Q x y = PeriodDomain.IsPositivePlane Q (PeriodDomain.framePlane (x, y))

def PeriodDomain.positiveFrames {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : Set (M × M)

The locus of ordered positive frames. It is not the positive-plane locus: different ordered bases can have the same image under framePlane.

Equations

• PeriodDomain.positiveFrames Q = {p : M × M | PeriodDomain.IsPositiveFrame Q p.1 p.2}

def PeriodDomain.pairingDet {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ x y : M) : ℝ

The 2 × 2 determinant of pairings of (x, y) against a reference pair (x₀, y₀). Up to the positive factor det of the reference Gram matrix this is the determinant of the orthogonal projection onto the reference plane, which is why its sign is an orientation.

Equations

• PeriodDomain.pairingDet Q x₀ y₀ x y = QuadraticMap.polar (⇑Q) x₀ x * QuadraticMap.polar (⇑Q) y₀ y - QuadraticMap.polar (⇑Q) x₀ y * QuadraticMap.polar (⇑Q) y₀ x

theorem PeriodDomain.isPositivePlane_framePlane {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {p : M × M} (h : p ∈ positiveFrames Q) : framePlane p ∈ positivePlanes Q

A positive frame forgets to a positive plane.

def PeriodDomain.forgetPositiveFrame {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (p : ↑(positiveFrames Q)) : ↑(positivePlanes Q)

The explicit forgetful map from ordered positive frames to unoriented positive planes. No inverse is chosen: a plane has many ordered bases.

Equations

• PeriodDomain.forgetPositiveFrame p = ⟨PeriodDomain.framePlane ↑p, ⋯⟩

@[simp]

theorem PeriodDomain.forgetPositiveFrame_coe {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (p : ↑(positiveFrames Q)) : ↑(forgetPositiveFrame p) = framePlane ↑p

theorem PeriodDomain.combination_ne_zero {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x y : M} (h : IsPositiveFrame Q x y) {a b : ℝ} (hab : a ≠ 0 ∨ b ≠ 0) : a • x + b • y ≠ 0

A nontrivial combination of a positive frame is nonzero: the frame spans a plane, so it is independent.

theorem PeriodDomain.pairingDet_ne_zero {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ x y : M} (h₀ : IsPositiveFrame Q x₀ y₀) (h : IsPositiveFrame Q x y) : pairingDet Q x₀ y₀ x y ≠ 0

The pairing determinant against a positive reference pair never vanishes.

A vanishing determinant produces a nonzero vector of the plane orthogonal to both reference vectors, hence in the reference plane's orthogonal complement, where Q is negative definite — while it lies in a plane where Q is positive definite. This is neg_of_mem_orthogonal in coordinates.

def PeriodDomain.SameOrientation {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ : M) (p q : M × M) : Prop

Two positive frames are similarly oriented when their determinants against the reference agree in sign.

The relation is stated against a fixed reference on purpose. That changing the reference either preserves every sign or flips every one — so that the partition is reference-free — is a genuine further statement: it is the cocycle identity for the projection signs. It is proved downstream, in QuadraticForm/PositiveFrameOrientation.lean, as sameOrientation_iff_of_reference; the proof there interpolates through positive frames rather than importing connectedness of the Grassmannian.

Equations

• PeriodDomain.SameOrientation Q x₀ y₀ p q = (0 < PeriodDomain.pairingDet Q x₀ y₀ p.1 p.2 * PeriodDomain.pairingDet Q x₀ y₀ q.1 q.2)

theorem PeriodDomain.sameOrientation_refl {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ : M} (h₀ : IsPositiveFrame Q x₀ y₀) {p : M × M} (hp : IsPositiveFrame Q p.1 p.2) : SameOrientation Q x₀ y₀ p p

theorem PeriodDomain.sameOrientation_symm {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x₀ y₀ : M} {p q : M × M} (h : SameOrientation Q x₀ y₀ p q) : SameOrientation Q x₀ y₀ q p

theorem PeriodDomain.sameOrientation_trans {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ : M} (h₀ : IsPositiveFrame Q x₀ y₀) {p q r : M × M} (hq : IsPositiveFrame Q q.1 q.2) (hpq : SameOrientation Q x₀ y₀ p q) (hqr : SameOrientation Q x₀ y₀ q r) : SameOrientation Q x₀ y₀ p r

theorem PeriodDomain.pairingDet_swap {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x₀ y₀ x y : M) : pairingDet Q x₀ y₀ y x = -pairingDet Q x₀ y₀ x y

Swapping the pair flips the sign: this is what makes the invariant an orientation rather than an arbitrary label.

theorem PeriodDomain.pairingDet_swap_ref {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x₀ y₀ x y : M) : pairingDet Q y₀ x₀ x y = -pairingDet Q x₀ y₀ x y

Swapping the reference pair flips the sign too.

def PeriodDomain.positiveFramesPlus {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ : M) : Set (M × M)

The positive half relative to a reference pair: P⁺ as far as this file can honestly define it.

Equations

• PeriodDomain.positiveFramesPlus Q x₀ y₀ = {p : M × M | PeriodDomain.IsPositiveFrame Q p.1 p.2 ∧ 0 < PeriodDomain.pairingDet Q x₀ y₀ p.1 p.2}

def PeriodDomain.positiveFramesMinus {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x₀ y₀ : M) : Set (M × M)

The other half.

Equations

• PeriodDomain.positiveFramesMinus Q x₀ y₀ = {p : M × M | PeriodDomain.IsPositiveFrame Q p.1 p.2 ∧ PeriodDomain.pairingDet Q x₀ y₀ p.1 p.2 < 0}

theorem PeriodDomain.disjoint_positiveFramesPlus_minus {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (x₀ y₀ : M) : Disjoint (positiveFramesPlus Q x₀ y₀) (positiveFramesMinus Q x₀ y₀)

theorem PeriodDomain.union_positiveFramesPlus_minus {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} [FiniteDimensional ℝ M] (hsig : HasSignatureTwo Q) {x₀ y₀ : M} (h₀ : IsPositiveFrame Q x₀ y₀) : positiveFrames Q = positiveFramesPlus Q x₀ y₀ ∪ positiveFramesMinus Q x₀ y₀

The two halves exhaust the positive frames. Nonvanishing of the determinant is what leaves no third case.

theorem PeriodDomain.swap_mem_of_mem_positiveFramesPlus {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} {x₀ y₀ : M} {p : M × M} (hp : p ∈ positiveFramesPlus Q x₀ y₀) : (p.2, p.1) ∈ positiveFramesMinus Q x₀ y₀

Swapping a pair moves it to the other half. So neither half is vacuous once one positive frame exists, and the split is a genuine two-way split.