leftUnitor_naturality — Mathlib

English

The right unitor is natural: for any f: M → N, tensorHom (f ⊗ id) ∘ rightUnitor(N) = rightUnitor(M) ∘ f.

Русский

Правый унитор естественен: для любого отображения f между модулями выполняется тождество натуральности правого унитора.

LaTeX

$$$\\mathrm{tensorHom}(f, \\mathrm{id}) \\; \\circ \\rho_N = \\rho_M \\; \\circ f$$$

Lean4

theorem leftUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
    tensorHom (𝟙 (ModuleCat.of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f :=
  by
  ext : 1
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext

  apply TensorProduct.ext
  ext x
  dsimp
  erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
  rw [LinearMap.map_smul]
  rfl

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