English
There is a root pairing associated to a bilinear form B, defined using the reflective vectors of B. This root pairing is a structured map from the set of reflective vectors to the dual of M, with a specified root and coroot behavior ensuring compatibility with reflections.
Русский
Существует парирование корней, связанное с bilinear-формой B, определённое через отражательные вектора B. Это парирование представляет собой структуру, отображающую множество отражательных векторов в двойственную пространство M*, удовлетворяющую условию совместимости с отражениями.
LaTeX
$$$$ \\text{RootPairing}_{B} : \\text{RootPairing}\\left( \\{\,x \\in M \\mid \\text{IsReflective}(B,x)\\} \\right) \\; R \\; M \\; (\\text{Dual } R M) $$$$
Lean4
/-- The root pairing given by all reflective vectors for a bilinear form. -/
def ofBilinear [IsReflexive R M] (B : M →ₗ[R] M →ₗ[R] R) (hNB : LinearMap.Nondegenerate B) (hSB : LinearMap.IsSymm B)
(h2 : IsRegular (2 : R)) : RootPairing {x : M | IsReflective B x} R M (Dual R M)
where
toLinearMap := Dual.eval R M
root := Embedding.subtype fun x ↦ IsReflective B x
coroot :=
{ toFun := fun x => IsReflective.coroot B x.2
inj' := by
intro x y hxy
simp only [mem_setOf_eq] at hxy
have h1 : ∀ z, IsReflective.coroot B x.2 z = IsReflective.coroot B y.2 z := fun z =>
congrFun (congrArg DFunLike.coe hxy) z
have h2x : ∀ z, B x x * IsReflective.coroot B x.2 z = B x x * IsReflective.coroot B y.2 z := fun z =>
congrArg (HMul.hMul ((B x) x)) (h1 z)
have h2y : ∀ z, B y y * IsReflective.coroot B x.2 z = B y y * IsReflective.coroot B y.2 z := fun z =>
congrArg (HMul.hMul ((B y) y)) (h1 z)
simp_rw [apply_self_mul_coroot_apply B x.2] at h2x
simp_rw [apply_self_mul_coroot_apply B y.2] at h2y
have h2xy : B x x = B y y := by
refine h2.1 ?_
dsimp only
specialize h2x y
rw [coroot_apply_self] at h2x
specialize h2y x
rw [coroot_apply_self] at h2y
rw [mul_comm, ← h2x, ← hSB.eq, RingHom.id_apply, ← h2y, mul_comm]
rw [Subtype.ext_iff, ← sub_eq_zero]
refine hNB.1 _ (fun z => ?_)
rw [map_sub, LinearMap.sub_apply, sub_eq_zero]
refine h2.1 ?_
dsimp only
rw [h2x z, ← h2y z, hxy, h2xy] }
root_coroot_two x := coroot_apply_self B x.2
reflectionPerm
x :=
{ toFun := fun y => ⟨(Module.reflection (coroot_apply_self B x.2) y), reflective_reflection B hSB x.2 y.2⟩
invFun := fun y => ⟨(Module.reflection (coroot_apply_self B x.2) y), reflective_reflection B hSB x.2 y.2⟩
left_inv := by
intro y
simp [involutive_reflection (coroot_apply_self B x.2) y]
right_inv := by
intro y
simp [involutive_reflection (coroot_apply_self B x.2) y] }
reflectionPerm_root x y := by simp [Module.reflection_apply]
reflectionPerm_coroot x
y :=
by
simp only [coe_setOf, mem_setOf_eq, Embedding.coeFn_mk, Embedding.subtype_apply, Dual.eval_apply, Equiv.coe_fn_mk]
ext z
simp only [sub_apply, smul_apply, smul_eq_mul]
refine y.2.1.1 ?_
simp only [mem_setOf_eq, mul_sub, apply_self_mul_coroot_apply B y.2, ← mul_assoc]
rw [← isOrthogonal_reflection B x.2 hSB y y, apply_self_mul_coroot_apply, ← hSB.eq z, ← hSB.eq z, RingHom.id_apply,
RingHom.id_apply, Module.reflection_apply, map_sub, mul_sub, sub_eq_sub_iff_comm, sub_left_inj]
refine x.2.1.1 ?_
simp only [mem_setOf_eq, map_smul, smul_eq_mul]
rw [← mul_assoc _ _ (B z x), ← mul_assoc _ _ (B z x), mul_left_comm, apply_self_mul_coroot_apply B x.2,
mul_left_comm (B x x), apply_self_mul_coroot_apply B x.2, ← hSB.eq x y, RingHom.id_apply, ← hSB.eq x z,
RingHom.id_apply]
ring
