quotientQuotientEquivQuotientAux_mk

English

The mk-mk compatibility expresses how lifts of MK through a chain of quotients behave with respect to the underlying quotient structure; in particular, lifting behaves well when passing to mk' maps.

Русский

Совместимость mk-мк выражает, как две стадии подъема через цепочку квартиований ведут себя по отношению к базовой структуре квотирования; в частности, подъем сохраняется при переходе к mk'.

LaTeX

$$$(\\text{QuotientQuotientEquivQuotientAux } N M h)(x) = \\text{mk}' M (x)$$$

Lean4

@[to_additive (attr := simp)]
theorem quotientQuotientEquivQuotientAux_mk (x : G ⧸ N) :
    quotientQuotientEquivQuotientAux N M h x = QuotientGroup.map N M (MonoidHom.id G) h x :=
  QuotientGroup.lift_mk' _ _ x

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