Reflection of binary quadratic forms

Reflection is the substitution (x, y) ↦ (x, -y), sending (a, b, c) to (a, -b, c). It is an involution, preserves content and discriminant, commutes with primitive normalization, and carries properly equivalent forms to properly equivalent forms, so it descends to the involution reflectedClass of the proper classes of primitive positive definite forms. These are the form-side operations needed by the improper-automorphism criterion for binary integral lattices.

def TauCeti.BinaryQuadraticForm.reflected {R : Type u_1} [Neg R] (f : BinaryQuadraticForm R) : BinaryQuadraticForm R

Reflection in the second variable of a binary quadratic form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.reflected_a {R : Type u_1} [Neg R] (f : BinaryQuadraticForm R) : f.reflected.a = f.a

@[simp]

theorem TauCeti.BinaryQuadraticForm.reflected_b {R : Type u_1} [Neg R] (f : BinaryQuadraticForm R) : f.reflected.b = -f.b

@[simp]

theorem TauCeti.BinaryQuadraticForm.reflected_c {R : Type u_1} [Neg R] (f : BinaryQuadraticForm R) : f.reflected.c = f.c

@[simp]

theorem TauCeti.BinaryQuadraticForm.reflected_reflected {R : Type u_1} [InvolutiveNeg R] (f : BinaryQuadraticForm R) : f.reflected.reflected = f

Reflecting twice gives the original form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.eval_reflected {R : Type u_1} [Ring R] (f : BinaryQuadraticForm R) (x y : R) : f.reflected.eval x y = f.eval x (-y)

Reflection is substitution of the negative second variable.

@[simp]

theorem TauCeti.BinaryQuadraticForm.discrim_reflected {R : Type u_1} [CommRing R] (f : BinaryQuadraticForm R) : f.reflected.discrim = f.discrim

Reflection preserves the discriminant.

@[simp]

theorem TauCeti.BinaryQuadraticForm.reflected_smul' {R : Type u_1} {S : Type u_2} [AddGroup R] [DistribSMul S R] (r : S) (f : BinaryQuadraticForm R) : (r • f).reflected = r • f.reflected

An external distributive scalar action on the coefficients commutes with reflection.

@[simp]

theorem TauCeti.BinaryQuadraticForm.content_reflected (f : BinaryQuadraticForm ℤ) : f.reflected.content = f.content

Reflection preserves the content of an integral form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.isPrimitive_reflected_iff (f : BinaryQuadraticForm ℤ) : f.reflected.IsPrimitive ↔ f.IsPrimitive

Reflection preserves primitivity of an integral binary form.

theorem TauCeti.BinaryQuadraticForm.reflected_mem_posDef_inf_primitiveForms_iff {n : ℕ} [NeZero n] {f : BinaryQuadraticForm ℤ} : f.reflected ∈ posDef n ⊓ primitiveForms (-↑n) ↔ f ∈ posDef n ⊓ primitiveForms (-↑n)

Reflection preserves the primitive positive definite forms of discriminant -n.

@[simp]

theorem TauCeti.BinaryQuadraticForm.primPart_reflected (f : BinaryQuadraticForm ℤ) : f.reflected.primPart = f.primPart.reflected

Primitive normalization commutes with reflection, including for the zero form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.reflected_smul {R : Type u_1} [CommRing R] (γ : Matrix.SpecialLinearGroup (Fin 2) R) (f : BinaryQuadraticForm R) : (γ • f).reflected = γ.conjJ • f.reflected

Reflection intertwines a proper change of variables with its canonical coordinate conjugate.

def TauCeti.BinaryQuadraticForm.reflectedClass (n : ℕ) [NeZero n] : PosDefProperClass n → PosDefProperClass n

The reflection (a, b, c) ↦ (a, -b, c) on proper classes of primitive positive definite forms of discriminant -n; it is well defined since reflected_smul carries properly equivalent forms to properly equivalent forms.

@[simp]

theorem TauCeti.BinaryQuadraticForm.reflectedClass_mk {n : ℕ} [NeZero n] (f : ↥(posDef n ⊓ primitiveForms (-↑n))) : reflectedClass n ⟦f⟧ = ⟦⟨(↑f).reflected, ⋯⟩⟧

The reflection of the class of a form is the class of the reflected form.

theorem TauCeti.BinaryQuadraticForm.reflectedClass_involutive (n : ℕ) [NeZero n] : Function.Involutive (reflectedClass n)

Reflection on proper classes is an involution.