English
If each component i has an isometry e_i between Q_i and Q'_i, then there is an isometry between pi Q and pi Q' built from the family e_i.
Русский
Если для каждой компоненты i есть изометрия e_i между Q_i и Q'_i, то между pi Q и pi Q' существует изометрия, составленная из e_i.
LaTeX
$$$ (\\forall i, (Q_i).IsometryEquiv (Q'_i)) \\Rightarrow (\\mathrm{pi}\\,Q).IsometryEquiv (\\mathrm{pi}\\,Q'). $$$
Lean4
/-- An isometry between quadratic forms generated by `QuadraticMap.pi` can be constructed
from a pair of isometries between the left and right parts. -/
@[simps toLinearEquiv]
def pi [Fintype ι] {Q : ∀ i, QuadraticMap R (Mᵢ i) P} {Q' : ∀ i, QuadraticMap R (Nᵢ i) P}
(e : ∀ i, (Q i).IsometryEquiv (Q' i)) : (pi Q).IsometryEquiv (pi Q')
where
map_app'
x := by simp only [pi_apply, LinearEquiv.piCongrRight, IsometryEquiv.coe_toLinearEquiv, IsometryEquiv.map_app]
toLinearEquiv := LinearEquiv.piCongrRight fun i => (e i : Mᵢ i ≃ₗ[R] Nᵢ i)
