§2.4, p. 20: $f=\eta_{\sqrt{-d}}$ commutes with the complex structure $I$ of $X\times\hat X$

Proved

MarkmanSecant.similarity_commutes_with_complex_structure

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

abelian-varietiesalgebraic-geometryhodge-theoryspinors

$f$ commutes with $I$ (Markman, arXiv:2502.03415, §2.4, p. 20; a consequence of Lemma 2.2.6).

Let $X$ be a complex torus of dimension $n$ with complex structure $J$ ( $J^2=-1$ ), let $d>0$ be rational and $\sqrt{-d}=i\sqrt d$ . Let $a,b$ lie in the Hodge ring $\bigoplus_pH^{p,p}(X,\mathbb{Q})$ , suppose that $\lambda_{1,2}=a\pm\sqrt{-d}\,b$ are even pure spinors with $W_1\cap W_2=0$ , and let $f$ be a rational endomorphism of $V_{\mathbb{Q}}$ acting by $\sqrt{-d}$ on $W_1$ and by $-\sqrt{-d}$ on $W_2$ . Then

f\circ I=I\circ f,

where $I=J\oplus(-J^{\mathsf T})$ is the complex structure of $V_{\mathbb{R}}=H^1(X\times\hat X,\mathbb{R})$ .

Consequently $f$ respects the complex structure of the torus $X\times\hat X$ , so $\eta(\sqrt{-d})=f$ embeds $K$ into $\operatorname{End}_{\mathbb{Q}}(X\times\hat X)$ .

Preamble

import Mathlib
import Definitions.Def_MarkmanSecant

open MarkmanSecant
open scoped ExteriorAlgebra

Formal statement

namespace MarkmanSecant

theorem similarity_commutes_with_complex_structure (n : ℕ)
    (J : Matrix (Fin (2 * n)) (Fin (2 * n)) ℝ) (hJ : J * J = -1)
    (d : ℚ) (hd : 0 < d) (a b : Spinor n)
    (ha : IsInHodgeRing J a) (hb : IsInHodgeRing J b)
    (h₁ : IsEvenPureSpinor (a + sqrtNeg d • b)) (h₂ : IsEvenPureSpinor (a - sqrtNeg d • b))
    (h₁₂ : annih (a + sqrtNeg d • b) ⊓ annih (a - sqrtNeg d • b) = ⊥)
    (F : Matrix (VIdx n) (VIdx n) ℚ)
    (hF₁ : ∀ v ∈ annih (a + sqrtNeg d • b), (ratMatV F).mulVec v = sqrtNeg d • v)
    (hF₂ : ∀ v ∈ annih (a - sqrtNeg d • b), (ratMatV F).mulVec v = (-sqrtNeg d) • v) :
    ratMatV F * IV J = IV J * ratMatV F := by sorry

end MarkmanSecant

Source

E. Markman, Cycles on abelian 2n-folds of Weil type from secant sheaves on abelian n-folds, arXiv:2502.03415v2 (8 Jun 2025), https://arxiv.org/abs/2502.03415

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements, with the source paper and the intended meaning in view. It is not independent testimony and must not be mistaken for a blind audit; an independent reviewer should re-derive what the code says before relying on it.

Read-back of MarkmanSecant.similarity_commutes_with_complex_structure.

Data and hypotheses: a natural number $n$ ; a real $2n\times2n$ matrix $J$ with $J^2=-1$ ; a rational $d>0$ ; spinors $a,b$ each in the Hodge ring for $J$ ; $\lambda_1=a+i\sqrt d\,b$ and $\lambda_2=a-i\sqrt d\,b$ even pure spinors; $\mathrm{annih}(\lambda_1)\cap\mathrm{annih}(\lambda_2)=\{0\}$ ; a rational $4n\times4n$ matrix $F$ with $F_{\mathbb{C}}v=i\sqrt d\,v$ for all $v\in\mathrm{annih}(\lambda_1)$ and $F_{\mathbb{C}}v=-i\sqrt d\,v$ for all $v\in\mathrm{annih}(\lambda_2)$ .

Claim: $F_{\mathbb{C}}\,I_V=I_V\,F_{\mathbb{C}}$ as complex matrices, where $I_V=\mathrm{diag}(J,-J^{\mathsf T})$ .

Human review

Endorsed by Shuze Chen · Sep 26, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

§2.4, p. 20: f=η−df=\eta_{\sqrt{-d}}f=η−d​​ commutes with the complex structure III of X×X^X\times\hat XX×X^

§2.4, p. 20: $f=\eta_{\sqrt{-d}}$ commutes with the complex structure $I$ of $X\times\hat X$