quotQuotEquivComm_comp_quotQuotMkₐ

English

The composition of double-quotient maps along the natural quotient MK maps equals the corresponding two-step quotient map, consistent with exchanging the roles of I and J.

Русский

Состав двойных отображений факторизации через естественный эквивалент MK равен соответствующему отображению двухступенчатого факторинга, при этом роли I и J меняются.

LaTeX

$$$\text{AlgHom}.comp (quotQuotEquivQuotOfLEₐ\, R\, I\, J) \ (quotQuotMkₐ\, R\, I\, J) = quotQuotMkₐ\, R\, J\, I$$$

Lean4

@[simp]
theorem quotQuotEquivComm_comp_quotQuotMkₐ :
    AlgHom.comp (↑(quotQuotEquivCommₐ R I J)) (quotQuotMkₐ R I J) = quotQuotMkₐ R J I :=
  AlgHom.ext <| quotQuotEquivComm_quotQuotMk I J

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