noncommProd

Stream: Is there code for X?

[Antoine Chambert-Loir]

There is docs#MonoidHom.noncommPiCoprod but that didn't seem to exist for a coproduct of two,
so I quickly wrote this this morning.

import Mathlib.Algebra.Group.Prod
import Mathlib.Tactic

/-! # Morphisms to a coproduct of two monoids -/
namespace MulHom

variable {M N P : Type*} [Mul M] [Mul N] [Semigroup P]
  (f : M →ₙ* P) (g : N →ₙ* P) (comm : ∀ m n, Commute (f m) (g n))

/-- Coproduct of two `MulHom`s with the same codomain:
`f.noncommCoprod g (p : M × N) = f p.1 * g p.2`. -/
@[to_additive
      "Coproduct of two `AddHom`s with the same codomain:
      `f.noncommCoprod g (p : M × N) = f p.1 + g p.2`."]
def noncommCoprod : M × N →ₙ* P where
  toFun := fun mn ↦ (f mn.fst) * (g mn.snd)
  map_mul' := fun mn mn' ↦ by
    simp only [Prod.fst_mul, Prod.snd_mul, map_mul]
    simp only [mul_assoc]
    apply congr_arg₂ _ rfl
    simp only [← mul_assoc]
    apply congr_arg₂ _ _ rfl
    apply comm

@[to_additive (attr := simp)]
theorem noncommCoprod_apply (p : M × N) :
  f.noncommCoprod g comm p = f p.1 * g p.2 :=
  rfl

@[to_additive (attr := simp)]
theorem noncommCoprod_apply' (p : M × N) :
    f.noncommCoprod g comm p = g p.2 * f p.1 :=
  comm p.1 p.2

@[to_additive]
theorem comp_noncommCoprod {Q : Type*} [Semigroup Q] (h : P →ₙ* Q) :
    h.comp (f.noncommCoprod g comm) =
      (h.comp f).noncommCoprod (h.comp g) (fun m n ↦ by
        simp only [coe_comp, Function.comp_apply]
        exact Commute.map (comm m n) h) :=
  ext fun x => by simp


end MulHom

namespace MonoidHom

variable {M N} [MulOneClass M] [MulOneClass N]

variable {P : Type*} [Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ m n, Commute (f m) (g n))

/-- Coproduct of two `MonoidHom`s with the same codomain:
`f.noncommCoprod g (p : M × N) = f p.1 * g p.2`. -/
@[to_additive
      "Coproduct of two `AddMonoidHom`s with the same codomain:
      `f.noncommCoprod g (p : M × N) = f p.1 + g p.2`."]
def noncommCoprod : M × N →* P where
  toFun := fun mn ↦ (f mn.fst) * (g mn.snd)
  map_mul' := fun mn mn' ↦ by
    simp only [Prod.fst_mul, Prod.snd_mul, map_mul]
    simp only [mul_assoc]
    apply congr_arg₂ _ rfl
    simp only [← mul_assoc]
    apply congr_arg₂ _ _ rfl
    apply comm
  map_one' := by
    simp only [Prod.fst_one, Prod.snd_one, map_one, mul_one]

@[to_additive (attr := simp)]
theorem noncommCoprod_apply (p : M × N) :
  f.noncommCoprod g comm p = f p.1 * g p.2 :=
  rfl

@[to_additive (attr := simp)]
theorem noncommCoprod_apply' (p : M × N) :
    f.noncommCoprod g comm p = g p.2 * f p.1 :=
  comm p.1 p.2

@[to_additive]
theorem comp_noncommCoprod {Q : Type*} [Monoid Q] (h : P →* Q) :
    h.comp (f.noncommCoprod g comm) =
      (h.comp f).noncommCoprod (h.comp g) (fun m n ↦ by
        simp only [coe_comp, Function.comp_apply]
        exact Commute.map (comm m n) h) :=
  ext fun x => by simp

end MonoidHom

[Eric Wieser]

Do we have docs#MonoidHom.coprod ?

[Antoine Chambert-Loir]

Yes, but it assumes commutativity of the target.

[Antoine Chambert-Loir]

(I should have said that, sorry…)

[Eric Wieser]

I think it's probably reasonable to PR the above; but make sure to reference it from the docstring of the .coprod version (and vice versa)

[Antoine Chambert-Loir]

Do you mean indicating that function in the docstring of the .coprod version (sth such as "commutative case") and conversely "for the commutative case, see…" ?

[Antoine Chambert-Loir]

PR : #7335