coprodCongr — Mathlib

English

Let e: M ≃* N and e': M' ≃* N' be monoid isomorphisms. Then the coproducts are also isomorphic: Coprod(M, M') ≃* Coprod(N, N'), induced by Coprod.map(e, e') with inverse Coprod.map(e^{-1}, (e')^{-1}). Equivalently, the universal construction of the coproduct is functorial in isomorphisms of the summands.

Русский

Пусть e: M ≃* N и e': M' ≃* N' — изоморфизмы моноидов. Тогда копродуктовые суммы эквивалентны: Coprod(M, M') ≃* Coprod(N, N'), индуцируемые Coprod.map(e, e') с обратным Coprod.map(e^{-1}, (e')^{-1}). Иными словами, конструкция копродукта сохраняет эквивариантность по отношению к изоморфизмам компонент.

LaTeX

$$$\\text{If } e: M \\simeq\\* N \\text{ and } e': M' \\simeq\\* N', \\text{ then } (M \\ast M') \\cong (N \\ast N') \\text{ via } Coprod.map(e,e') \\text{ with inverse } Coprod.map(e.RelSymm, e'.RelSymm).$$$

Lean4

/-- Lift two monoid equivalences `e : M ≃* N` and `e' : M' ≃* N'` to a monoid equivalence
`(M ∗ M') ≃* (N ∗ N')`. -/
@[to_additive (attr := simps! -fullyApplied) /-- Lift two additive monoid
    equivalences `e : M ≃+ N` and `e' : M' ≃+ N'` to an additive monoid equivalence
    `(AddMonoid.Coprod M M') ≃+ (AddMonoid.Coprod N N')`. -/
    ]
def coprodCongr (e : M ≃* N) (e' : M' ≃* N') : (M ∗ M') ≃* (N ∗ N') :=
  (Coprod.map (e : M →* N) (e' : M' →* N')).toMulEquiv (Coprod.map e.symm e'.symm) (by ext <;> simp) (by ext <;> simp)

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