dualProdIsometry — Mathlib

English

Given a linear equivalence f: M ≃ₗ[R] N, there is a quadratic map IsometryEquiv between dualProd on M and dualProd on N, transported along f.

Русский

Существуют квадратичные изометрии между dualProd на M и на N, получаемые перенесением через линейное эквивалентное отображение f: M ≃ N.

LaTeX

$$dualProdIsometry (f) : (dualProd R M) ≈ Isometry (dualProd R N)$$

Lean4

/-- Any module isomorphism induces a quadratic isomorphism between the corresponding `dual_prod.` -/
@[simps!]
def dualProdIsometry (f : M ≃ₗ[R] N) : (dualProd R M).IsometryEquiv (dualProd R N)
    where
  toLinearEquiv := f.dualMap.symm.prodCongr f
  map_app' x := DFunLike.congr_arg x.fst <| f.symm_apply_apply _

Похожие утверждения