Reflection in a vector of norm minus two

For a module M over a commutative ring R with a bilinear form B, and a vector s with B s s = -2, the map

ρ_s(v) = v + B v s • s

is the reflection in the hyperplane s^⊥. The -2 is what makes the usual formula v - 2⟪v,s⟫/⟪s,s⟫ · s integral: the denominator cancels the 2, so no division is needed and the reflection is defined on the module rather than on its rationalisation.

This is stated over an arbitrary ambient form, not over one extension

Lattice/Mukai/Reflection.lean used to own this argument on the single carrier ℤ × N × ℤ, even though nothing in it is about that carrier: every step is bilinearity, symmetry, or the one hypothesis B s s = -2. It is restated here on (R, M, B), and the Mukai file specialises it at B := Mukai.pairingBilin b. There is one reflection, not two.

This is not the spherical twist. On a K3 surface the Seidel--Thomas twist T_E acts on the Mukai lattice as ρ_{v(E)}, and that statement is the eventual reason this theory exists. But T_E is an autoequivalence of Dᵇ(Coh X), its construction needs an evaluation triangle and a functorial cone, and none of that is available here or asserted here.

Which hypothesis does what

The split is not the expected one, and stating it over an arbitrary form is what makes it visible:

• additivity needs neither symmetry of B nor B s s = -2. It is bilinearity alone, so reflectHom is a linear map for every s;
• involutivity needs B s s = -2 and nothing else;
• isometry needs symmetry of B as well, and fails without it -- the two cross terms only cancel against B v s * B w s * B s s once they are equal.

-2 is the hypothesis rather than a IsSpherical-style predicate on purpose: spherical-class vocabulary is application vocabulary, and it stays with the application.

def BilinearForm.reflect {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s v : M) : M

Reflection in s: ρ_s(v) = v + B v s • s.

For B s s = -2 this is the reflection in s^⊥; for other s it is still a well-defined additive map, but is neither an involution nor an isometry. The definition deliberately takes no hypothesis so that reflectHom below is available unconditionally.

Equations

• BilinearForm.reflect B s v = v + (B v) s • s

theorem BilinearForm.reflect_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s v : M) : reflect B s v = v + (B v) s • s

@[simp]

theorem BilinearForm.reflect_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) : reflect B s 0 = 0

theorem BilinearForm.reflect_add {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s v w : M) : reflect B s (v + w) = reflect B s v + reflect B s w

theorem BilinearForm.reflect_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (a : R) (s v : M) : reflect B s (a • v) = a • reflect B s v

theorem BilinearForm.reflect_neg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s v : M) : reflect B s (-v) = -reflect B s v

def BilinearForm.reflectHom {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) : M →ₗ[R] M

ρ_s as a linear endomorphism.

No hypothesis on s: additivity is bilinearity of B, nothing more.

Equations

• BilinearForm.reflectHom B s = { toFun := BilinearForm.reflect B s, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem BilinearForm.reflectHom_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s v : M) : (reflectHom B s) v = reflect B s v

theorem BilinearForm.apply_reflect_right {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) (v : M) : (B (reflect B s v)) s = -(B v) s

theorem BilinearForm.reflect_reflect {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) (v : M) : reflect B s (reflect B s v) = v

theorem BilinearForm.reflect_involutive {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) : Function.Involutive (reflect B s)

theorem BilinearForm.reflect_bijective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) : Function.Bijective (reflect B s)

def BilinearForm.reflectEquiv {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) : M ≃ₗ[R] M

ρ_s as a linear automorphism, with itself as inverse. Needs B s s = -2, which is what makes it an involution.

Equations

• BilinearForm.reflectEquiv B s hs = { toLinearMap := BilinearForm.reflectHom B s, invFun := BilinearForm.reflect B s, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem BilinearForm.reflectEquiv_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) (v : M) : (reflectEquiv B s hs) v = reflect B s v

@[simp]

theorem BilinearForm.reflectEquiv_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) (v : M) : (reflectEquiv B s hs).symm v = reflect B s v

@[simp]

theorem BilinearForm.reflect_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) : reflect B s s = -s

theorem BilinearForm.reflect_of_apply_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) {s v : M} (h : (B v) s = 0) : reflect B s v = v

theorem BilinearForm.apply_reflect_eq_zero_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s : M) (hs : (B s) s = -2) (v : M) : (B (reflect B s v)) s = 0 ↔ (B v) s = 0

theorem BilinearForm.apply_reflect_reflect {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (s : M) (hs : (B s) s = -2) (v w : M) : (B (reflect B s v)) (reflect B s w) = (B v) w

theorem BilinearForm.self_reflect {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (s : M) (hs : (B s) s = -2) (v : M) : (B (reflect B s v)) (reflect B s v) = (B v) v

def BilinearForm.reflectIsometry {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (s : M) (hs : (B s) s = -2) : B →bᵢ B

ρ_s as an isometry of B. This is the first statement to need symmetry of B as well as B s s = -2.

Equations

• BilinearForm.reflectIsometry B hb s hs = { toLinearMap := BilinearForm.reflectHom B s, map_app' := ⋯ }

@[simp]

theorem BilinearForm.reflectIsometry_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (hb : ∀ (x y : M), (B x) y = (B y) x) (s : M) (hs : (B s) s = -2) (v : M) : (reflectIsometry B hb s hs) v = reflect B s v

@[simp]

theorem BilinearForm.reflect_neg_left {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : M →ₗ[R] M →ₗ[R] R) (s v : M) : reflect B (-s) v = reflect B s v