instSMulUnitsIntIso — Mathlib

English

In a preadditive category, a scalar coming from Units(Z) acts compatibly on isomorphisms: a • e maps to a • e.hom and a⁻¹ • e.inv on the inverse.

Русский

В преддобавительной категории скалар из Units(ℤ) действует на изоморфизма e так, что (a • e).hom = a • e.hom и (a • e).inv = a⁻¹ • e.inv.

LaTeX

$$forall (a : Units ℤ) (e : X ≅ Y), (a • e).hom = a • e.hom ∧ (a • e).inv = a⁻¹ • e.inv$$

Lean4

instance : SMul (Units ℤ) (X ≅ Y) where
  smul a
    e :=
    { hom := (a : ℤ) • e.hom
      inv := ((a⁻¹ : Units ℤ) : ℤ) • e.inv
      hom_inv_id := by simp only [comp_zsmul, zsmul_comp, smul_smul, Units.inv_mul, one_smul, e.hom_inv_id]
      inv_hom_id := by simp only [comp_zsmul, zsmul_comp, smul_smul, Units.mul_inv, one_smul, e.inv_hom_id] }

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