lift_comp_comm_eq — Mathlib

English

A compatibility between lift and the commutativity isomorphism: lifting f after swapping M and N equals lifting the flipped f.

Русский

Совместимость между поднятием и изоморфизмом перестановки факторов: поднятие f после замены M и N эквивалентно поднятию f с развёртыванием.

LaTeX

$$$\\mathrm{lift}\\ f \\circ\\mathrm{comm}_{R}(N,M) = \\mathrm{lift}\\ f.rename^{\\mathrm{flip}}$$$

Lean4

theorem lift_comp_comm_eq (f : M →ₗ[R] N →ₗ[R] P) : lift f ∘ₗ TensorProduct.comm R N M = lift f.flip :=
  ext rfl

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