Hodge-index data for a symmetric real pairing

DivisorSpace is the established name of a real vector space equipped with a symmetric bilinear pairing. HodgeIndex records the index inequality relative to a positive vector, while HodgeDefinite records negative definiteness on its orthogonal complement. The latter determines the signature and nondegeneracy of the pairing.

All declarations in this file are linear algebra. No charge family, Chern character, scheme, support predicate, or wall arrangement is imported. The existing namespace is preserved by the ownership cutover.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace (D : Type w) [AddCommGroup D] [Module ℝ D] : Type w

A real vector space with a symmetric bilinear pairing.

• intersection : LinearMap.BilinForm ℝ D

  The real intersection pairing.

• intersection_symm : self.intersection.IsSymm

  The pairing is symmetric.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.pair {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (x y : D) : ℝ

Dot notation for the symmetric pairing.

Equations

• S.pair x y = (S.intersection x) y

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.pair_apply {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (x y : D) : S.pair x y = (S.intersection x) y

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.pair_comm {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (x y : D) : S.pair x y = S.pair y x

Symmetry of the pairing.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.pair_zero_left {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (x : D) : S.pair 0 x = 0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.pair_zero_right {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (x : D) : S.pair x 0 = 0

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.HodgeIndex {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H : D) : Prop

The Hodge index inequality relative to a vector H of positive square.

• H_square_pos : 0 < S.pair H H

  The reference vector has positive square.

• index_le (x : D) : S.pair H H * S.pair x x ≤ S.pair H x ^ 2

  The index inequality at every vector.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.HodgeIndex.pair_self_nonpos_of_orthogonal {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {H : D} (h : S.HodgeIndex H) {x : D} (hx : S.pair H x = 0) : S.pair x x ≤ 0

A vector orthogonal to H has nonpositive square.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.HodgeIndex.pair_self_neg_of_orthogonal {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {H : D} (h : S.HodgeIndex H) {x : D} (hx : S.pair H x = 0) (hne : S.pair x x ≠ 0) : S.pair x x < 0

An orthogonal vector with nonzero square has negative square.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.HodgeDefinite {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H : D) : Prop

Negative definiteness on H^⊥, together with positivity of H².

• H_square_pos : 0 < S.pair H H

  The reference vector has positive square.

• neg_definite (x : D) : S.pair H x = 0 → x ≠ 0 → S.pair x x < 0

  The form is negative definite on the orthogonal complement of H.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.HodgeDefinite.toHodgeIndex {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {H : D} (h : S.HodgeDefinite H) : S.HodgeIndex H

Definiteness on H^⊥ implies the Hodge index inequality.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.intersectionQuadratic {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) : QuadraticForm ℝ D

The self-pairing bundled as a quadratic form.

Equations

• S.intersectionQuadratic = LinearMap.BilinMap.toQuadraticMap S.intersection

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.intersectionQuadratic_apply {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (x : D) : S.intersectionQuadratic x = S.pair x x

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.polar_intersectionQuadratic {D : Type w} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (x y : D) : QuadraticMap.polar (⇑S.intersectionQuadratic) x y = 2 * S.pair x y

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.sigPos_sigNeg_of_hodgeDefinite {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {H : D} [FiniteDimensional ℝ D] (h : S.HodgeDefinite H) : sigPos S.intersectionQuadratic = 1 ∧ sigNeg S.intersectionQuadratic + 1 = Module.finrank ℝ D

The indices of inertia of a Hodge-definite pairing.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.nondegenerate_of_hodgeDefinite {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {H : D} [FiniteDimensional ℝ D] (h : S.HodgeDefinite H) : QuadraticMap.Nondegenerate

A Hodge-definite pairing is nondegenerate.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.HodgeDefinite.of_pair_pos {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {H : D} [FiniteDimensional ℝ D] (h : S.HodgeDefinite H) {omega : D} (homega : 0 < S.pair omega omega) : S.HodgeDefinite omega

A Hodge-definite certificate can be transported to any positive vector.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorSpace.hasSignatureTwo_of_hodgeDefinite {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {H : D} [FiniteDimensional ℝ D] (h : S.HodgeDefinite H) : PeriodDomain.HasSignatureTwo (Mukai.realForm S.intersection)

The real Mukai extension of a Hodge-definite pairing has signature two.