symm — Mathlib

English

There is a symmetric isomorphism between pushout constructions when swapping the middle algebras.

Русский

Существуют симметрические преобразования между пушаут-структурами при перестановке центральных алгебр.

LaTeX

$$Algebra.IsPushout.symm$$

Lean4

@[symm]
theorem symm (h : Algebra.IsPushout R S R' S') : Algebra.IsPushout R R' S S' where
  out :=
    .of_equiv
      { __ := (TensorProduct.comm R ..).toAddEquiv.trans (equiv R S R' S').toAddEquiv,
        map_smul' _
          x :=
          x.induction_on (by simp) (fun _ _ ↦ by simp [equiv_tmul, Algebra.smul_def, mul_left_comm])
            (by simp +contextual) }
      fun _ ↦ by simp [equiv_tmul]

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