English
Let e be a basis of a finite free module M over a commutative ring R. For any family w of units indexed by the basis, twisting e by the units w produces a new basis whose orientation is the reciprocal of the product of the w_i, scaled from the original orientation.
Русский
Пусть e — базис модуля M над кольцом R, и задано отображение w: ι → Units(R). Базис e, модифицированный умножением на единицы w, имеет ориентацию равную обратному произведению всех w_i, умноженному на ориентацию исходного базиса.
LaTeX
$$$$(e.{\\rm unitsSMul\\}\\,w).\\mathrm{orientation} = \\Big(\\prod_i w_i\\Big)^{-1} \\;\\cdot\\; e.{\\rm orientation}$$$$
Lean4
/-- The orientation given by a basis derived using `units_smul`, in terms of the product of those
units. -/
theorem orientation_unitsSMul (e : Basis ι R M) (w : ι → Units R) :
(e.unitsSMul w).orientation = (∏ i, w i)⁻¹ • e.orientation :=
by
rw [Basis.orientation, Basis.orientation, smul_rayOfNeZero, ray_eq_iff, e.det.eq_smul_basis_det (e.unitsSMul w),
det_unitsSMul_self, Units.smul_def, smul_smul]
norm_cast
simp only [inv_mul_cancel, Units.val_one, one_smul]
exact SameRay.rfl
