Mathlib.Algebra.Group.Prod

Prod.one_mk_mul_one_mk theorem

[MulOneClass M] [Mul N] (b₁ b₂ : N) : ((1 : M), b₁) * (1, b₂) = (1, b₁ * b₂)

Full source

@[to_additive]
theorem one_mk_mul_one_mk [MulOneClass M] [Mul N] (b₁ b₂ : N) :
    ((1 : M), b₁) * (1, b₂) = (1, b₁ * b₂) := by
  rw [mk_mul_mk, mul_one]

Product of identity-pairs in $M \times N$ simplifies to identity and product

Informal description

Let $M$ be a type with a multiplicative structure that has a one element (i.e., $M$ is a `MulOneClass`), and let $N$ be a type with a multiplication operation. For any elements $b₁, b₂ \in N$, the product of the pairs $(1_M, b₁)$ and $(1_M, b₂)$ in $M \times N$ is equal to $(1_M, b₁ * b₂)$, where $1_M$ is the one element of $M$ and $*$ is the multiplication in $N$.

Prod.mk_one_mul_mk_one theorem

[Mul M] [MulOneClass N] (a₁ a₂ : M) : (a₁, (1 : N)) * (a₂, 1) = (a₁ * a₂, 1)

Full source

@[to_additive]
theorem mk_one_mul_mk_one [Mul M] [MulOneClass N] (a₁ a₂ : M) :
    (a₁, (1 : N)) * (a₂, 1) = (a₁ * a₂, 1) := by
  rw [mk_mul_mk, mul_one]

Product of Elements with Identity in Second Component

Informal description

Let $M$ be a type with a multiplication operation and $N$ be a type with a multiplication operation and a multiplicative identity. For any elements $a_1, a_2 \in M$, the product $(a_1, 1) \cdot (a_2, 1)$ in $M \times N$ equals $(a_1 \cdot a_2, 1)$, where $1$ denotes the multiplicative identity in $N$.

Prod.fst_mul_snd theorem

[MulOneClass M] [MulOneClass N] (p : M × N) : (p.fst, 1) * (1, p.snd) = p

Full source

@[to_additive]
theorem fst_mul_snd [MulOneClass M] [MulOneClass N] (p : M × N) : (p.fst, 1) * (1, p.snd) = p :=
  Prod.ext (mul_one p.1) (one_mul p.2)

Decomposition of Product Group Element via First and Second Components

Informal description

Let $M$ and $N$ be multiplicative monoids (i.e., types with an associative binary operation and an identity element). For any element $p = (m, n) \in M \times N$, the product $(m, 1) \cdot (1, n)$ equals $p$.

Prod.instInvolutiveInv instance

[InvolutiveInv M] [InvolutiveInv N] : InvolutiveInv (M × N)

Full source

@[to_additive]
instance [InvolutiveInv M] [InvolutiveInv N] : InvolutiveInv (M × N) :=
  { inv_inv := fun _ => Prod.ext (inv_inv _) (inv_inv _) }

Involutive Inversion on Product Types

Informal description

For any types $M$ and $N$ equipped with an involutive inversion operation (i.e., an operation satisfying $x^{-1^{-1}} = x$), the product type $M \times N$ also has an involutive inversion operation defined componentwise.

Prod.instSemigroup instance

[Semigroup M] [Semigroup N] : Semigroup (M × N)

Full source

@[to_additive]
instance instSemigroup [Semigroup M] [Semigroup N] : Semigroup (M × N) where
  mul_assoc _ _ _ := by ext <;> exact mul_assoc ..

Product of Semigroups is a Semigroup

Informal description

For any two semigroups $M$ and $N$, the product $M \times N$ is also a semigroup with componentwise multiplication.

Prod.instCommSemigroup instance

[CommSemigroup G] [CommSemigroup H] : CommSemigroup (G × H)

Full source

@[to_additive]
instance instCommSemigroup [CommSemigroup G] [CommSemigroup H] : CommSemigroup (G × H) where
  mul_comm _ _ := by ext <;> exact mul_comm ..

Product of Commutative Semigroups is a Commutative Semigroup

Informal description

For any two commutative semigroups $G$ and $H$, the product $G \times H$ is also a commutative semigroup with componentwise multiplication.

Prod.instMulOneClass instance

[MulOneClass M] [MulOneClass N] : MulOneClass (M × N)

Full source

@[to_additive]
instance instMulOneClass [MulOneClass M] [MulOneClass N] : MulOneClass (M × N) where
  one_mul _ := by ext <;> exact one_mul _
  mul_one _ := by ext <;> exact mul_one _

Componentwise `MulOneClass` Structure on Product Types

Informal description

For any two types $M$ and $N$ each equipped with a `MulOneClass` structure (i.e., a multiplicative structure with a unit element), the product type $M \times N$ also carries a `MulOneClass` structure where multiplication is defined componentwise and the unit is the pair of units $(1,1)$.

Prod.instMonoid instance

[Monoid M] [Monoid N] : Monoid (M × N)

Full source

@[to_additive]
instance instMonoid [Monoid M] [Monoid N] : Monoid (M × N) :=
  { npow := fun z a => ⟨Monoid.npow z a.1, Monoid.npow z a.2⟩,
    npow_zero := fun _ => Prod.ext (Monoid.npow_zero _) (Monoid.npow_zero _),
    npow_succ := fun _ _ => Prod.ext (Monoid.npow_succ _ _) (Monoid.npow_succ _ _),
    one_mul := by simp,
    mul_one := by simp }

Product of Monoids is a Monoid

Informal description

For any two monoids $M$ and $N$, the product $M \times N$ is also a monoid with componentwise multiplication and identity element $(1, 1)$.

Prod.instDivInvMonoid instance

[DivInvMonoid G] [DivInvMonoid H] : DivInvMonoid (G × H)

Full source

@[to_additive Prod.subNegMonoid]
instance [DivInvMonoid G] [DivInvMonoid H] : DivInvMonoid (G × H) where
  div_eq_mul_inv _ _ := by ext <;> exact div_eq_mul_inv ..
  zpow z a := ⟨DivInvMonoid.zpow z a.1, DivInvMonoid.zpow z a.2⟩
  zpow_zero' _ := by ext <;> exact DivInvMonoid.zpow_zero' _
  zpow_succ' _ _ := by ext <;> exact DivInvMonoid.zpow_succ' ..
  zpow_neg' _ _ := by ext <;> exact DivInvMonoid.zpow_neg' ..

Product of Div-Invariant Monoids is a Div-Invariant Monoid

Informal description

For any two div-invariant monoids $G$ and $H$, the product $G \times H$ is also a div-invariant monoid with componentwise division and inversion operations.

Prod.instDivisionMonoid instance

[DivisionMonoid G] [DivisionMonoid H] : DivisionMonoid (G × H)

Full source

@[to_additive]
instance [DivisionMonoid G] [DivisionMonoid H] : DivisionMonoid (G × H) :=
  { mul_inv_rev := fun _ _ => Prod.ext (mul_inv_rev _ _) (mul_inv_rev _ _),
    inv_eq_of_mul := fun _ _ h =>
      Prod.ext (inv_eq_of_mul_eq_one_right <| congr_arg fst h)
        (inv_eq_of_mul_eq_one_right <| congr_arg snd h),
    inv_inv := by simp }

Product of Division Monoids is a Division Monoid

Informal description

For any two division monoids $G$ and $H$, the product $G \times H$ is also a division monoid with componentwise division and inversion operations.

Prod.instDivisionCommMonoid instance

[DivisionCommMonoid G] [DivisionCommMonoid H] : DivisionCommMonoid (G × H)

Full source

@[to_additive SubtractionCommMonoid]
instance [DivisionCommMonoid G] [DivisionCommMonoid H] : DivisionCommMonoid (G × H) :=
  { mul_comm := fun ⟨g₁ , h₁⟩ ⟨_, _⟩ => by rw [mk_mul_mk, mul_comm g₁, mul_comm h₁]; rfl }

Product of Commutative Division Monoids is a Commutative Division Monoid

Informal description

For any two commutative division monoids $G$ and $H$, the product $G \times H$ is also a commutative division monoid with componentwise division and inversion operations.

Prod.instGroup instance

[Group G] [Group H] : Group (G × H)

Full source

@[to_additive]
instance instGroup [Group G] [Group H] : Group (G × H) where
  inv_mul_cancel _ := by ext <;> exact inv_mul_cancel _

Product of Groups is a Group

Informal description

For any groups $G$ and $H$, the product $G \times H$ is also a group with componentwise multiplication and inversion operations.

Prod.instIsLeftCancelMul instance

[Mul G] [Mul H] [IsLeftCancelMul G] [IsLeftCancelMul H] : IsLeftCancelMul (G × H)

Full source

@[to_additive]
instance [Mul G] [Mul H] [IsLeftCancelMul G] [IsLeftCancelMul H] : IsLeftCancelMul (G × H) where
  mul_left_cancel _ _ _ h :=
      Prod.ext (mul_left_cancel (Prod.ext_iff.1 h).1) (mul_left_cancel (Prod.ext_iff.1 h).2)

Left Cancellation Property for Product of Multiplicative Structures

Informal description

For any types $G$ and $H$ with multiplication operations and left cancellation properties, the product type $G \times H$ also has the left cancellation property for multiplication. That is, for any $(a, b), (c, d), (e, f) \in G \times H$, if $(a, b) * (c, d) = (a, b) * (e, f)$, then $(c, d) = (e, f)$.

Prod.instIsRightCancelMul instance

[Mul G] [Mul H] [IsRightCancelMul G] [IsRightCancelMul H] : IsRightCancelMul (G × H)

Full source

@[to_additive]
instance [Mul G] [Mul H] [IsRightCancelMul G] [IsRightCancelMul H] : IsRightCancelMul (G × H) where
  mul_right_cancel _ _ _ h :=
      Prod.ext (mul_right_cancel (Prod.ext_iff.1 h).1) (mul_right_cancel (Prod.ext_iff.1 h).2)

Right Cancellation Property for Product of Multiplicative Structures

Informal description

For any types $G$ and $H$ equipped with multiplication operations and the right cancellation property, the product type $G \times H$ also has the right cancellation property for multiplication. That is, if $(a, c) \cdot (b, c) = (a', c) \cdot (b, c)$ for any $(a, c), (a', c), (b, c) \in G \times H$, then $(a, c) = (a', c)$.

Prod.instIsCancelMul instance

[Mul G] [Mul H] [IsCancelMul G] [IsCancelMul H] : IsCancelMul (G × H)

Full source

@[to_additive]
instance [Mul G] [Mul H] [IsCancelMul G] [IsCancelMul H] : IsCancelMul (G × H) where

Cancellation Property for Product of Multiplicative Structures

Informal description

For any types $G$ and $H$ equipped with multiplication operations and the cancellation property (both left and right cancellation), the product type $G \times H$ also has the cancellation property for multiplication. That is, for any $(a, b), (c, d), (e, f) \in G \times H$, if $(a, b) * (c, d) = (a, b) * (e, f)$, then $(c, d) = (e, f)$, and similarly for right cancellation.

Prod.instLeftCancelSemigroup instance

[LeftCancelSemigroup G] [LeftCancelSemigroup H] : LeftCancelSemigroup (G × H)

Full source

@[to_additive]
instance [LeftCancelSemigroup G] [LeftCancelSemigroup H] : LeftCancelSemigroup (G × H) :=
  { mul_left_cancel := fun _ _ _ => mul_left_cancel }

Product of Left-Cancellative Semigroups is Left-Cancellative

Informal description

For any two left-cancellative semigroups $G$ and $H$, the product $G \times H$ is also a left-cancellative semigroup with componentwise multiplication.

Prod.instRightCancelSemigroup instance

[RightCancelSemigroup G] [RightCancelSemigroup H] : RightCancelSemigroup (G × H)

Full source

@[to_additive]
instance [RightCancelSemigroup G] [RightCancelSemigroup H] : RightCancelSemigroup (G × H) :=
  { mul_right_cancel := fun _ _ _ => mul_right_cancel }

Product of Right-Cancellative Semigroups is Right-Cancellative

Informal description

For any two right-cancellative semigroups $G$ and $H$, the product $G \times H$ is also a right-cancellative semigroup with componentwise multiplication.

Prod.instLeftCancelMonoid instance

[LeftCancelMonoid M] [LeftCancelMonoid N] : LeftCancelMonoid (M × N)

Full source

@[to_additive]
instance [LeftCancelMonoid M] [LeftCancelMonoid N] : LeftCancelMonoid (M × N) :=
  { mul_one := by simp,
    one_mul := by simp
    mul_left_cancel := by simp }

Product of Left-Cancellative Monoids is Left-Cancellative

Informal description

For any two left-cancellative monoids $M$ and $N$, the product $M \times N$ is also a left-cancellative monoid with componentwise multiplication.

Prod.instRightCancelMonoid instance

[RightCancelMonoid M] [RightCancelMonoid N] : RightCancelMonoid (M × N)

Full source

@[to_additive]
instance [RightCancelMonoid M] [RightCancelMonoid N] : RightCancelMonoid (M × N) :=
  { mul_one := by simp,
    one_mul := by simp
    mul_right_cancel := by simp }

Product of Right-Cancellative Monoids is Right-Cancellative

Informal description

For any two right-cancellative monoids $M$ and $N$, the product $M \times N$ is also a right-cancellative monoid with componentwise multiplication.

Prod.instCancelMonoid instance

[CancelMonoid M] [CancelMonoid N] : CancelMonoid (M × N)

Full source

@[to_additive]
instance [CancelMonoid M] [CancelMonoid N] : CancelMonoid (M × N) :=
  { mul_right_cancel := by simp only [mul_left_inj, imp_self, forall_const] }

Product of Cancellative Monoids is Cancellative

Informal description

For any two cancellative monoids $M$ and $N$, the product $M \times N$ is also a cancellative monoid with componentwise multiplication.

Prod.instCommMonoid instance

[CommMonoid M] [CommMonoid N] : CommMonoid (M × N)

Full source

@[to_additive]
instance instCommMonoid [CommMonoid M] [CommMonoid N] : CommMonoid (M × N) :=
  { mul_comm := fun ⟨m₁, n₁⟩ ⟨_, _⟩ => by rw [mk_mul_mk, mk_mul_mk, mul_comm m₁, mul_comm n₁] }

Product of Commutative Monoids is a Commutative Monoid

Informal description

For any two commutative monoids $M$ and $N$, the product $M \times N$ is also a commutative monoid with componentwise multiplication and identity element $(1, 1)$.

Prod.instCancelCommMonoid instance

[CancelCommMonoid M] [CancelCommMonoid N] : CancelCommMonoid (M × N)

Full source

@[to_additive]
instance [CancelCommMonoid M] [CancelCommMonoid N] : CancelCommMonoid (M × N) :=
  { mul_left_cancel := by simp }

Product of Cancellative Commutative Monoids is Cancellative Commutative

Informal description

For any two cancellative commutative monoids $M$ and $N$, the product $M \times N$ is also a cancellative commutative monoid with componentwise multiplication.

Prod.instCommGroup instance

[CommGroup G] [CommGroup H] : CommGroup (G × H)

Full source

@[to_additive]
instance instCommGroup [CommGroup G] [CommGroup H] : CommGroup (G × H) :=
  { mul_comm := fun ⟨g₁, h₁⟩ ⟨_, _⟩ => by rw [mk_mul_mk, mk_mul_mk, mul_comm g₁, mul_comm h₁] }

Product of Commutative Groups is a Commutative Group

Informal description

For any commutative groups $G$ and $H$, the product $G \times H$ is also a commutative group with componentwise multiplication and inversion operations.

SemiconjBy.prod theorem

{x y z : M × N} (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) : SemiconjBy x y z

Full source

@[to_additive AddSemiconjBy.prod]
theorem SemiconjBy.prod {x y z : M × N}
    (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) : SemiconjBy x y z :=
  Prod.ext hm hn

Semiconjugacy in Product Monoids

Informal description

Let $x, y, z$ be elements of the product monoid $M \times N$. If $x_1 \cdot y_1 = y_1 \cdot z_1$ holds in $M$ and $x_2 \cdot y_2 = y_2 \cdot z_2$ holds in $N$, then $(x_1, x_2) \cdot (y_1, y_2) = (y_1, y_2) \cdot (z_1, z_2)$ holds in $M \times N$.

Prod.semiconjBy_iff theorem

{x y z : M × N} : SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2

Full source

@[to_additive]
theorem Prod.semiconjBy_iff {x y z : M × N} :
    SemiconjBySemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2 := Prod.ext_iff

Semiconjugacy in Product Monoid Decomposes Componentwise

Informal description

For elements $x = (x_1, x_2)$, $y = (y_1, y_2)$, and $z = (z_1, z_2)$ in the product monoid $M \times N$, the following are equivalent: 1. $x$ semiconjugates $y$ to $z$ (i.e., $x * y = z * x$ holds in $M \times N$) 2. $x_1$ semiconjugates $y_1$ to $z_1$ in $M$ and $x_2$ semiconjugates $y_2$ to $z_2$ in $N$

Commute.prod theorem

{x y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y

Full source

@[to_additive AddCommute.prod]
theorem Commute.prod {x y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y :=
  SemiconjBy.prod hm hn

Commutation in Product Monoid via Componentwise Commutation

Informal description

Let $x = (x_1, x_2)$ and $y = (y_1, y_2)$ be elements of the product monoid $M \times N$. If $x_1$ commutes with $y_1$ in $M$ and $x_2$ commutes with $y_2$ in $N$, then $x$ commutes with $y$ in $M \times N$.

Prod.commute_iff theorem

{x y : M × N} : Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2

Full source

@[to_additive]
theorem Prod.commute_iff {x y : M × N} :
    CommuteCommute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2 := semiconjBy_iff

Commutation in Product Monoid Decomposes Componentwise

Informal description

For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product monoid $M \times N$, the following are equivalent: 1. $x$ and $y$ commute (i.e., $x * y = y * x$ holds in $M \times N$) 2. $x_1$ and $y_1$ commute in $M$ and $x_2$ and $y_2$ commute in $N$

MulHom.fst definition

: M × N →ₙ* M

Full source

/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `M`. -/
@[to_additive
      "Given additive magmas `A`, `B`, the natural projection homomorphism
      from `A × B` to `A`"]
def fst : M × NM × N →ₙ* M :=
  ⟨Prod.fst, fun _ _ => rfl⟩

First projection as a multiplicative homomorphism

Informal description

Given magmas $ M $ and $ N $, the function $ \text{fst} : M \times N \to M $ is a multiplicative homomorphism that projects the first component of a pair $ (x, y) $ to $ x $.

MulHom.snd definition

: M × N →ₙ* N

Full source

/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `N`. -/
@[to_additive
      "Given additive magmas `A`, `B`, the natural projection homomorphism
      from `A × B` to `B`"]
def snd : M × NM × N →ₙ* N :=
  ⟨Prod.snd, fun _ _ => rfl⟩

Second projection homomorphism of product magmas

Informal description

The natural projection homomorphism from the product of magmas $ M \times N $ to $ N $, which maps each pair $(x, y)$ to its second component $ y $. This map preserves the multiplicative structure.

MulHom.coe_fst theorem

: ⇑(fst M N) = Prod.fst

Full source

@[to_additive (attr := simp)]
theorem coe_fst : ⇑(fst M N) = Prod.fst :=
  rfl

First Projection Homomorphism as Standard Projection

Informal description

The underlying function of the first projection multiplicative homomorphism $\text{fst} : M \times N \to M$ is equal to the standard first projection function $\text{Prod.fst} : M \times N \to M$.

MulHom.coe_snd theorem

: ⇑(snd M N) = Prod.snd

Full source

@[to_additive (attr := simp)]
theorem coe_snd : ⇑(snd M N) = Prod.snd :=
  rfl

Second Projection Homomorphism as Standard Projection

Informal description

The underlying function of the second projection multiplicative homomorphism $\text{snd} \colon M \times N \to N$ is equal to the standard second projection function $\text{Prod.snd} \colon M \times N \to N$.

MulHom.prod definition

(f : M →ₙ* N) (g : M →ₙ* P) : M →ₙ* N × P

Full source

/-- Combine two `MonoidHom`s `f : M →ₙ* N`, `g : M →ₙ* P` into
`f.prod g : M →ₙ* (N × P)` given by `(f.prod g) x = (f x, g x)`. -/
@[to_additive prod
      "Combine two `AddMonoidHom`s `f : AddHom M N`, `g : AddHom M P` into
      `f.prod g : AddHom M (N × P)` given by `(f.prod g) x = (f x, g x)`"]
protected def prod (f : M →ₙ* N) (g : M →ₙ* P) :
    M →ₙ* N × P where
  toFun := Pi.prod f g
  map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y)

Product of multiplicative homomorphisms

Informal description

Given two multiplicative homomorphisms $f \colon M \to N$ and $g \colon M \to P$, the function $\text{MulHom.prod} \, f \, g \colon M \to N \times P$ is defined by $(\text{MulHom.prod} \, f \, g)(x) = (f(x), g(x))$ for all $x \in M$. This function is itself a multiplicative homomorphism.

MulHom.coe_prod theorem

(f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Pi.prod f g

Full source

@[to_additive coe_prod]
theorem coe_prod (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Pi.prod f g :=
  rfl

Coefficient of Product Homomorphism Equals Pointwise Product Function

Informal description

For any multiplicative homomorphisms $f \colon M \to N$ and $g \colon M \to P$, the underlying function of the product homomorphism $f \times g \colon M \to N \times P$ is equal to the pointwise product function $\Pi.\text{prod} \, f \, g$, which maps each $x \in M$ to $(f(x), g(x))$.

MulHom.prod_apply theorem

(f : M →ₙ* N) (g : M →ₙ* P) (x) : f.prod g x = (f x, g x)

Full source

@[to_additive (attr := simp) prod_apply]
theorem prod_apply (f : M →ₙ* N) (g : M →ₙ* P) (x) : f.prod g x = (f x, g x) :=
  rfl

Evaluation of Product Homomorphism: $(f \times g)(x) = (f(x), g(x))$

Informal description

For any multiplicative homomorphisms $f \colon M \to N$ and $g \colon M \to P$, and for any element $x \in M$, the product homomorphism $(f \times g)(x)$ evaluates to $(f(x), g(x))$.

MulHom.fst_comp_prod theorem

(f : M →ₙ* N) (g : M →ₙ* P) : (fst N P).comp (f.prod g) = f

Full source

@[to_additive (attr := simp) fst_comp_prod]
theorem fst_comp_prod (f : M →ₙ* N) (g : M →ₙ* P) : (fst N P).comp (f.prod g) = f :=
  ext fun _ => rfl

First Projection of Product Homomorphism Equals First Factor

Informal description

For any multiplicative homomorphisms $f \colon M \to N$ and $g \colon M \to P$, the composition of the first projection homomorphism $\text{fst} \colon N \times P \to N$ with the product homomorphism $f \times g \colon M \to N \times P$ equals $f$. That is, $\text{fst} \circ (f \times g) = f$.

MulHom.snd_comp_prod theorem

(f : M →ₙ* N) (g : M →ₙ* P) : (snd N P).comp (f.prod g) = g

Full source

@[to_additive (attr := simp) snd_comp_prod]
theorem snd_comp_prod (f : M →ₙ* N) (g : M →ₙ* P) : (snd N P).comp (f.prod g) = g :=
  ext fun _ => rfl

Second Projection of Product Homomorphism Equals Second Factor

Informal description

For any multiplicative homomorphisms $f \colon M \to N$ and $g \colon M \to P$, the composition of the second projection homomorphism $\text{snd} \colon N \times P \to P$ with the product homomorphism $f \times g \colon M \to N \times P$ equals $g$. That is, $\text{snd} \circ (f \times g) = g$.

MulHom.prod_unique theorem

(f : M →ₙ* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f

Full source

@[to_additive (attr := simp) prod_unique]
theorem prod_unique (f : M →ₙ* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Uniqueness of Product Homomorphism Decomposition

Informal description

For any multiplicative homomorphism $f \colon M \to N \times P$, the product of the composition of $f$ with the first projection $\text{fst} \colon N \times P \to N$ and the composition of $f$ with the second projection $\text{snd} \colon N \times P \to P$ is equal to $f$ itself. In other words, $(\text{fst} \circ f) \times (\text{snd} \circ f) = f$.

MulHom.prodMap definition

: M × N →ₙ* M' × N'

Full source

/-- `Prod.map` as a `MonoidHom`. -/
@[to_additive prodMap "`Prod.map` as an `AddMonoidHom`"]
def prodMap : M × NM × N →ₙ* M' × N' :=
  (f.comp (fst M N)).prod (g.comp (snd M N))

Product map of multiplicative homomorphisms

Informal description

Given multiplicative homomorphisms $ f \colon M \to M' $ and $ g \colon N \to N' $, the function $ \text{MulHom.prodMap} \, f \, g \colon M \times N \to M' \times N' $ is defined by $ (\text{MulHom.prodMap} \, f \, g)(x, y) = (f(x), g(y)) $ for all $ (x, y) \in M \times N $. This function is itself a multiplicative homomorphism.

MulHom.prodMap_def theorem

: prodMap f g = (f.comp (fst M N)).prod (g.comp (snd M N))

Full source

@[to_additive prodMap_def]
theorem prodMap_def : prodMap f g = (f.comp (fst M N)).prod (g.comp (snd M N)) :=
  rfl

Definition of Product Map via Projections and Composition

Informal description

Given multiplicative homomorphisms $f \colon M \to M'$ and $g \colon N \to N'$, the product map $\text{prodMap} \, f \, g \colon M \times N \to M' \times N'$ is equal to the product of the composition of $f$ with the first projection $\text{fst} \colon M \times N \to M$ and the composition of $g$ with the second projection $\text{snd} \colon M \times N \to N$. That is, \[ \text{prodMap} \, f \, g = (f \circ \text{fst}) \times (g \circ \text{snd}). \]

MulHom.coe_prodMap theorem

: ⇑(prodMap f g) = Prod.map f g

Full source

@[to_additive (attr := simp) coe_prodMap]
theorem coe_prodMap : ⇑(prodMap f g) = Prod.map f g :=
  rfl

Product map of multiplicative homomorphisms equals product of functions

Informal description

Given multiplicative homomorphisms $f \colon M \to M'$ and $g \colon N \to N'$, the underlying function of the product map $\text{prodMap}\, f\, g \colon M \times N \to M' \times N'$ is equal to the product of the functions $f$ and $g$, i.e., \[ \text{prodMap}\, f\, g = (f \times g). \]

MulHom.prod_comp_prodMap theorem

 (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :
  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

Full source

@[to_additive prod_comp_prodMap]
theorem prod_comp_prodMap (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :
    (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
  rfl

Composition of Product Maps Equals Product of Compositions for Multiplicative Homomorphisms

Informal description

Given multiplicative homomorphisms $f \colon P \to M$, $g \colon P \to N$, $f' \colon M \to M'$, and $g' \colon N \to N'$, the composition of the product map $(f' \times g')$ with the product homomorphism $(f \times g)$ is equal to the product of the compositions $(f' \circ f) \times (g' \circ g)$. That is, $$ (f' \times g') \circ (f \times g) = (f' \circ f) \times (g' \circ g). $$

MulHom.coprod definition

: M × N →ₙ* P

Full source

/-- Coproduct of two `MulHom`s with the same codomain:
  `f.coprod g (p : M × N) = f p.1 * g p.2`.
  (Commutative codomain; for the general case, see `MulHom.noncommCoprod`) -/
@[to_additive
    "Coproduct of two `AddHom`s with the same codomain:
    `f.coprod g (p : M × N) = f p.1 + g p.2`.
    (Commutative codomain; for the general case, see `AddHom.noncommCoprod`)"]
def coprod : M × NM × N →ₙ* P :=
  f.comp (fst M N) * g.comp (snd M N)

Coproduct of multiplicative homomorphisms

Informal description

Given multiplicative homomorphisms $ f: M \to P $ and $ g: N \to P $ where $ P $ is a commutative semigroup, the coproduct homomorphism $ f \cdot g: M \times N \to P $ is defined by $(x, y) \mapsto f(x) \cdot g(y)$. This combines the two homomorphisms into a single homomorphism on the product structure.

MulHom.coprod_apply theorem

(p : M × N) : f.coprod g p = f p.1 * g p.2

Full source

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

Evaluation of Coproduct Homomorphism: $(f \cdot g)(x, y) = f(x) \cdot g(y)$

Informal description

For any multiplicative homomorphisms $f \colon M \to P$ and $g \colon N \to P$ where $P$ is a commutative semigroup, and for any pair $(x, y) \in M \times N$, the coproduct homomorphism satisfies $(f \cdot g)(x, y) = f(x) \cdot g(y)$.

MulHom.comp_coprod theorem

 {Q : Type*} [CommSemigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :
  h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

Full source

@[to_additive]
theorem comp_coprod {Q : Type*} [CommSemigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :
    h.comp (f.coprod g) = (h.comp f).coprod (h.comp g) :=
  ext fun x => by simp

Composition of Coproduct Homomorphism with a Multiplicative Homomorphism

Informal description

Let $Q$ be a commutative semigroup, and let $h \colon P \to Q$ be a multiplicative homomorphism. For any multiplicative homomorphisms $f \colon M \to P$ and $g \colon N \to P$, the composition of $h$ with the coproduct homomorphism $f \cdot g$ is equal to the coproduct of the compositions $h \circ f$ and $h \circ g$. In other words, $h \circ (f \cdot g) = (h \circ f) \cdot (h \circ g)$.

MonoidHom.fst definition

: M × N →* M

Full source

/-- Given monoids `M`, `N`, the natural projection homomorphism from `M × N` to `M`. -/
@[to_additive
      "Given additive monoids `A`, `B`, the natural projection homomorphism
      from `A × B` to `A`"]
def fst : M × NM × N →* M :=
  { toFun := Prod.fst,
    map_one' := rfl,
    map_mul' := fun _ _ => rfl }

First projection monoid homomorphism

Informal description

The monoid homomorphism from the product monoid $ M \times N $ to $ M $ that projects onto the first component. It maps the identity element $(1,1)$ to $1$ and preserves multiplication, i.e., $(x_1, y_1) \cdot (x_2, y_2)$ is mapped to $x_1 \cdot x_2$.

MonoidHom.snd definition

: M × N →* N

Full source

/-- Given monoids `M`, `N`, the natural projection homomorphism from `M × N` to `N`. -/
@[to_additive
      "Given additive monoids `A`, `B`, the natural projection homomorphism
      from `A × B` to `B`"]
def snd : M × NM × N →* N :=
  { toFun := Prod.snd,
    map_one' := rfl,
    map_mul' := fun _ _ => rfl }

Second projection monoid homomorphism

Informal description

The monoid homomorphism from the product monoid $ M \times N $ to the monoid $ N $, which projects onto the second component. It maps the identity element $(1, 1)$ to $1$ and preserves multiplication, i.e., $(x_1, y_1) \cdot (x_2, y_2) = (x_1 x_2, y_1 y_2)$ is sent to $y_1 y_2$.

MonoidHom.inl definition

: M →* M × N

Full source

/-- Given monoids `M`, `N`, the natural inclusion homomorphism from `M` to `M × N`. -/
@[to_additive
      "Given additive monoids `A`, `B`, the natural inclusion homomorphism
      from `A` to `A × B`."]
def inl : M →* M × N :=
  { toFun := fun x => (x, 1),
    map_one' := rfl,
    map_mul' := fun _ _ => Prod.ext rfl (one_mul 1).symm }

Left inclusion monoid homomorphism

Informal description

For monoids $M$ and $N$, the natural inclusion homomorphism from $M$ to $M \times N$ maps an element $x \in M$ to $(x, 1_N)$, where $1_N$ is the identity element of $N$.

MonoidHom.inr definition

: N →* M × N

Full source

/-- Given monoids `M`, `N`, the natural inclusion homomorphism from `N` to `M × N`. -/
@[to_additive
      "Given additive monoids `A`, `B`, the natural inclusion homomorphism
      from `B` to `A × B`."]
def inr : N →* M × N :=
  { toFun := fun y => (1, y),
    map_one' := rfl,
    map_mul' := fun _ _ => Prod.ext (one_mul 1).symm rfl }

Inclusion homomorphism into the second component of a product monoid

Informal description

For monoids $ M $ and $ N $, the natural inclusion homomorphism from $ N $ to $ M \times N $ that maps an element $ y \in N $ to $ (1, y) $, where $ 1 $ is the identity element of $ M $. This homomorphism preserves the multiplicative identity and the operation.

MonoidHom.coe_fst theorem

: ⇑(fst M N) = Prod.fst

Full source

@[to_additive (attr := simp)]
theorem coe_fst : ⇑(fst M N) = Prod.fst :=
  rfl

First Projection Monoid Homomorphism as Standard Projection

Informal description

The underlying function of the first projection monoid homomorphism $\text{fst} : M \times N \to M$ is equal to the standard first projection function $\text{Prod.fst} : M \times N \to M$.

MonoidHom.coe_snd theorem

: ⇑(snd M N) = Prod.snd

Full source

@[to_additive (attr := simp)]
theorem coe_snd : ⇑(snd M N) = Prod.snd :=
  rfl

Second Projection Monoid Homomorphism as Standard Projection

Informal description

The underlying function of the second projection monoid homomorphism `snd : M × N →* N` is equal to the standard second projection function `Prod.snd : M × N → N`.

MonoidHom.inl_apply theorem

(x) : inl M N x = (x, 1)

Full source

@[to_additive (attr := simp)]
theorem inl_apply (x) : inl M N x = (x, 1) :=
  rfl

Left inclusion homomorphism maps to element and identity

Informal description

For monoids $M$ and $N$, the left inclusion homomorphism $\mathrm{inl} \colon M \to M \times N$ maps any element $x \in M$ to the pair $(x, 1_N)$, where $1_N$ is the identity element of $N$.

MonoidHom.inr_apply theorem

(y) : inr M N y = (1, y)

Full source

@[to_additive (attr := simp)]
theorem inr_apply (y) : inr M N y = (1, y) :=
  rfl

Right inclusion homomorphism maps to identity and element

Informal description

For monoids $M$ and $N$, the right inclusion homomorphism $\text{inr} : N \to M \times N$ maps any element $y \in N$ to the pair $(1, y) \in M \times N$, where $1$ is the identity element of $M$.

MonoidHom.fst_comp_inl theorem

: (fst M N).comp (inl M N) = id M

Full source

@[to_additive (attr := simp)]
theorem fst_comp_inl : (fst M N).comp (inl M N) = id M :=
  rfl

First projection composed with left inclusion is identity

Informal description

For monoids $M$ and $N$, the composition of the first projection homomorphism $\mathrm{fst} \colon M \times N \to M$ with the left inclusion homomorphism $\mathrm{inl} \colon M \to M \times N$ equals the identity homomorphism on $M$.

MonoidHom.snd_comp_inl theorem

: (snd M N).comp (inl M N) = 1

Full source

@[to_additive (attr := simp)]
theorem snd_comp_inl : (snd M N).comp (inl M N) = 1 :=
  rfl

Composition of Second Projection with Left Inclusion Yields Trivial Homomorphism

Informal description

For monoids $M$ and $N$, the composition of the second projection homomorphism $\text{snd} : M \times N \to N$ with the left inclusion homomorphism $\text{inl} : M \to M \times N$ yields the trivial homomorphism $1 : M \to N$.

MonoidHom.fst_comp_inr theorem

: (fst M N).comp (inr M N) = 1

Full source

@[to_additive (attr := simp)]
theorem fst_comp_inr : (fst M N).comp (inr M N) = 1 :=
  rfl

Composition of First Projection with Right Inclusion Yields Trivial Homomorphism

Informal description

For monoids $M$ and $N$, the composition of the first projection homomorphism $\text{fst} : M \times N \to M$ with the right inclusion homomorphism $\text{inr} : N \to M \times N$ yields the trivial homomorphism $1 : N \to M$.

MonoidHom.snd_comp_inr theorem

: (snd M N).comp (inr M N) = id N

Full source

@[to_additive (attr := simp)]
theorem snd_comp_inr : (snd M N).comp (inr M N) = id N :=
  rfl

Composition of Second Projection with Right Inclusion Yields Identity

Informal description

For monoids $M$ and $N$, the composition of the second projection homomorphism $\text{snd} : M \times N \to N$ with the right inclusion homomorphism $\text{inr} : N \to M \times N$ yields the identity homomorphism on $N$.

MonoidHom.commute_inl_inr theorem

(m : M) (n : N) : Commute (inl M N m) (inr M N n)

Full source

@[to_additive]
theorem commute_inl_inr (m : M) (n : N) : Commute (inl M N m) (inr M N n) :=
  Commute.prod (.one_right m) (.one_left n)

Commutation of Left and Right Inclusion Homomorphisms in Product Monoid

Informal description

For any elements $m \in M$ and $n \in N$ in monoids $M$ and $N$ respectively, the images of $m$ under the left inclusion homomorphism $\text{inl} : M \to M \times N$ and $n$ under the right inclusion homomorphism $\text{inr} : N \to M \times N$ commute in the product monoid $M \times N$. That is, $(m, 1_N) \cdot (1_M, n) = (1_M, n) \cdot (m, 1_N)$.

MonoidHom.prod definition

(f : M →* N) (g : M →* P) : M →* N × P

Full source

/-- Combine two `MonoidHom`s `f : M →* N`, `g : M →* P` into `f.prod g : M →* N × P`
given by `(f.prod g) x = (f x, g x)`. -/
@[to_additive prod
      "Combine two `AddMonoidHom`s `f : M →+ N`, `g : M →+ P` into
      `f.prod g : M →+ N × P` given by `(f.prod g) x = (f x, g x)`"]
protected def prod (f : M →* N) (g : M →* P) :
    M →* N × P where
  toFun := Pi.prod f g
  map_one' := Prod.ext f.map_one g.map_one
  map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y)

Product of monoid homomorphisms

Informal description

Given two monoid homomorphisms $ f : M \to N $ and $ g : M \to P $, the function $ f \times g : M \to N \times P $ defined by $ (f \times g)(x) = (f(x), g(x)) $ is also a monoid homomorphism.

MonoidHom.coe_prod theorem

(f : M →* N) (g : M →* P) : ⇑(f.prod g) = Pi.prod f g

Full source

@[to_additive coe_prod]
theorem coe_prod (f : M →* N) (g : M →* P) : ⇑(f.prod g) = Pi.prod f g :=
  rfl

Coefficient of Product Homomorphism Equals Pointwise Product

Informal description

For any two monoid homomorphisms $f \colon M \to N$ and $g \colon M \to P$, the underlying function of the product homomorphism $f \times g \colon M \to N \times P$ is equal to the pointwise product of the functions $f$ and $g$, i.e., $(f \times g)(x) = (f(x), g(x))$ for all $x \in M$.

MonoidHom.prod_apply theorem

(f : M →* N) (g : M →* P) (x) : f.prod g x = (f x, g x)

Full source

@[to_additive (attr := simp) prod_apply]
theorem prod_apply (f : M →* N) (g : M →* P) (x) : f.prod g x = (f x, g x) :=
  rfl

Evaluation of Product Homomorphism Equals Componentwise Evaluation

Informal description

For any monoid homomorphisms $f \colon M \to N$ and $g \colon M \to P$, and any element $x \in M$, the evaluation of the product homomorphism $f \times g$ at $x$ is equal to $(f(x), g(x))$.

MonoidHom.fst_comp_prod theorem

(f : M →* N) (g : M →* P) : (fst N P).comp (f.prod g) = f

Full source

@[to_additive (attr := simp) fst_comp_prod]
theorem fst_comp_prod (f : M →* N) (g : M →* P) : (fst N P).comp (f.prod g) = f :=
  ext fun _ => rfl

First projection of product homomorphism equals first factor

Informal description

For any monoid homomorphisms $f \colon M \to N$ and $g \colon M \to P$, the composition of the first projection homomorphism $\mathrm{fst} \colon N \times P \to N$ with the product homomorphism $f \times g \colon M \to N \times P$ equals $f$.

MonoidHom.snd_comp_prod theorem

(f : M →* N) (g : M →* P) : (snd N P).comp (f.prod g) = g

Full source

@[to_additive (attr := simp) snd_comp_prod]
theorem snd_comp_prod (f : M →* N) (g : M →* P) : (snd N P).comp (f.prod g) = g :=
  ext fun _ => rfl

Second projection of product homomorphism equals second factor

Informal description

For any monoid homomorphisms $f \colon M \to N$ and $g \colon M \to P$, the composition of the second projection homomorphism $\mathrm{snd} \colon N \times P \to P$ with the product homomorphism $f \times g \colon M \to N \times P$ equals $g$.

MonoidHom.prod_unique theorem

(f : M →* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f

Full source

@[to_additive (attr := simp) prod_unique]
theorem prod_unique (f : M →* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f :=
  ext fun x => by simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Uniqueness of Product Homomorphism via Projections

Informal description

For any monoid homomorphism $f \colon M \to N \times P$, the product of the composition of $f$ with the first projection $\mathrm{fst} \colon N \times P \to N$ and the composition of $f$ with the second projection $\mathrm{snd} \colon N \times P \to P$ equals $f$ itself. In other words, $(\mathrm{fst} \circ f) \times (\mathrm{snd} \circ f) = f$.

MonoidHom.prodMap definition

: M × N →* M' × N'

Full source

/-- `Prod.map` as a `MonoidHom`. -/
@[to_additive prodMap "`Prod.map` as an `AddMonoidHom`."]
def prodMap : M × NM × N →* M' × N' :=
  (f.comp (fst M N)).prod (g.comp (snd M N))

Product map of monoid homomorphisms

Informal description

The monoid homomorphism from the product monoid $ M \times N $ to $ M' \times N' $ that applies $ f $ to the first component and $ g $ to the second component. It maps $(x, y)$ to $(f(x), g(y))$ and preserves the monoid structure.

MonoidHom.prodMap_def theorem

: prodMap f g = (f.comp (fst M N)).prod (g.comp (snd M N))

Full source

@[to_additive prodMap_def]
theorem prodMap_def : prodMap f g = (f.comp (fst M N)).prod (g.comp (snd M N)) :=
  rfl

Definition of Product Map via Projections

Informal description

The product map of monoid homomorphisms $f \colon M \to M'$ and $g \colon N \to N'$ is equal to the product of the composition of $f$ with the first projection $\mathrm{fst} \colon M \times N \to M$ and the composition of $g$ with the second projection $\mathrm{snd} \colon M \times N \to N$. In other words, \[ \mathrm{prodMap}\, f\, g = (f \circ \mathrm{fst}) \times (g \circ \mathrm{snd}). \]

MonoidHom.coe_prodMap theorem

: ⇑(prodMap f g) = Prod.map f g

Full source

@[to_additive (attr := simp) coe_prodMap]
theorem coe_prodMap : ⇑(prodMap f g) = Prod.map f g :=
  rfl

Product Map of Monoid Homomorphisms as Function Pair

Informal description

The underlying function of the product map of monoid homomorphisms $f \colon M \to M'$ and $g \colon N \to N'$ is equal to the product map of the underlying functions, i.e., $\mathrm{prodMap}\, f\, g = \mathrm{Prod.map}\, f\, g$.

MonoidHom.prod_comp_prodMap theorem

 (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :
  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

Full source

@[to_additive prod_comp_prodMap]
theorem prod_comp_prodMap (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :
    (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
  rfl

Composition of Product Maps Equals Product of Compositions

Informal description

Given monoid homomorphisms $f \colon P \to M$, $g \colon P \to N$, $f' \colon M \to M'$, and $g' \colon N \to N'$, the composition of the product map $(f' \times g')$ with the product homomorphism $(f \times g)$ is equal to the product of the compositions $(f' \circ f) \times (g' \circ g)$. In other words, \[ (f' \times g') \circ (f \times g) = (f' \circ f) \times (g' \circ g). \]

MonoidHom.coprod definition

: M × N →* P

Full source

/-- Coproduct of two `MonoidHom`s with the same codomain:
  `f.coprod g (p : M × N) = f p.1 * g p.2`.
  (Commutative case; for the general case, see `MonoidHom.noncommCoprod`.) -/
@[to_additive
    "Coproduct of two `AddMonoidHom`s with the same codomain:
    `f.coprod g (p : M × N) = f p.1 + g p.2`.
    (Commutative case; for the general case, see `AddHom.noncommCoprod`.)"]
def coprod : M × NM × N →* P :=
  f.comp (fst M N) * g.comp (snd M N)

Commutative coproduct of monoid homomorphisms

Informal description

Given two monoid homomorphisms $f \colon M \to P$ and $g \colon N \to P$ where $P$ is commutative, the coproduct homomorphism $f \cdot g \colon M \times N \to P$ is defined by $(x, y) \mapsto f(x) \cdot g(y)$. This combines $f$ and $g$ into a single homomorphism on the product monoid $M \times N$.

MonoidHom.coprod_apply theorem

(p : M × N) : f.coprod g p = f p.1 * g p.2

Full source

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

Evaluation of Coproduct Homomorphism: $(f \cdot g)(x, y) = f(x) \cdot g(y)$

Informal description

For any monoid homomorphisms $f \colon M \to P$ and $g \colon N \to P$ where $P$ is commutative, and any element $(x, y) \in M \times N$, the coproduct homomorphism $f \cdot g$ satisfies $(f \cdot g)(x, y) = f(x) \cdot g(y)$.

MonoidHom.coprod_comp_inl theorem

: (f.coprod g).comp (inl M N) = f

Full source

@[to_additive (attr := simp)]
theorem coprod_comp_inl : (f.coprod g).comp (inl M N) = f :=
  ext fun x => by simp [coprod_apply]

Composition of coproduct homomorphism with left inclusion equals first homomorphism

Informal description

For monoid homomorphisms $f \colon M \to P$ and $g \colon N \to P$ where $P$ is commutative, the composition of the coproduct homomorphism $f \cdot g \colon M \times N \to P$ with the left inclusion homomorphism $\text{inl} \colon M \to M \times N$ equals $f$. That is, $(f \cdot g) \circ \text{inl} = f$.

MonoidHom.coprod_comp_inr theorem

: (f.coprod g).comp (inr M N) = g

Full source

@[to_additive (attr := simp)]
theorem coprod_comp_inr : (f.coprod g).comp (inr M N) = g :=
  ext fun x => by simp [coprod_apply]

Composition of coproduct homomorphism with right inclusion equals second homomorphism

Informal description

For monoid homomorphisms $f \colon M \to P$ and $g \colon N \to P$ where $P$ is commutative, the composition of the coproduct homomorphism $f \cdot g \colon M \times N \to P$ with the right inclusion homomorphism $\text{inr} \colon N \to M \times N$ equals $g$. That is, $(f \cdot g) \circ \text{inr} = g$.

MonoidHom.coprod_unique theorem

(f : M × N →* P) : (f.comp (inl M N)).coprod (f.comp (inr M N)) = f

Full source

@[to_additive (attr := simp)]
theorem coprod_unique (f : M × NM × N →* P) : (f.comp (inl M N)).coprod (f.comp (inr M N)) = f :=
  ext fun x => by simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

Uniqueness of coproduct decomposition for monoid homomorphisms

Informal description

For any monoid homomorphism $f \colon M \times N \to P$, the coproduct of the compositions of $f$ with the left and right inclusion homomorphisms equals $f$ itself. That is, $(f \circ \text{inl}) \cdot (f \circ \text{inr}) = f$, where $\text{inl} \colon M \to M \times N$ and $\text{inr} \colon N \to M \times N$ are the inclusion homomorphisms.

MonoidHom.coprod_inl_inr theorem

{M N : Type*} [CommMonoid M] [CommMonoid N] : (inl M N).coprod (inr M N) = id (M × N)

Full source

@[to_additive (attr := simp)]
theorem coprod_inl_inr {M N : Type*} [CommMonoid M] [CommMonoid N] :
    (inl M N).coprod (inr M N) = id (M × N) :=
  coprod_unique (id <| M × N)

Coproduct of Inclusion Homomorphisms Equals Identity on Product Monoid

Informal description

For any two commutative monoids $M$ and $N$, the coproduct of the left inclusion homomorphism $\text{inl} \colon M \to M \times N$ and the right inclusion homomorphism $\text{inr} \colon N \to M \times N$ equals the identity homomorphism on $M \times N$. That is, $\text{inl} \cdot \text{inr} = \text{id}_{M \times N}$.

MonoidHom.comp_coprod theorem

 {Q : Type*} [CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) : h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

Full source

@[to_additive]
theorem comp_coprod {Q : Type*} [CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :
    h.comp (f.coprod g) = (h.comp f).coprod (h.comp g) :=
  ext fun x => by simp

Composition with Coproduct of Monoid Homomorphisms

Informal description

Let $M$, $N$, $P$, and $Q$ be commutative monoids. Given monoid homomorphisms $h \colon P \to Q$, $f \colon M \to P$, and $g \colon N \to P$, the composition of $h$ with the coproduct homomorphism $f \cdot g$ is equal to the coproduct of the compositions $h \circ f$ and $h \circ g$. In other words, the following diagram commutes: $$ h \circ (f \cdot g) = (h \circ f) \cdot (h \circ g) $$

MulEquiv.prodComm definition

: M × N ≃* N × M

Full source

/-- The equivalence between `M × N` and `N × M` given by swapping the components
is multiplicative. -/
@[to_additive prodComm
      "The equivalence between `M × N` and `N × M` given by swapping the
      components is additive."]
def prodComm : M × NM × N ≃* N × M :=
  { Equiv.prodComm M N with map_mul' := fun ⟨_, _⟩ ⟨_, _⟩ => rfl }

Multiplicative equivalence of product monoids by component swapping

Informal description

The multiplicative equivalence between the product monoids $ M \times N $ and $ N \times M $ is given by swapping the components, i.e., mapping $ (x, y) $ to $ (y, x) $. This equivalence preserves the multiplicative structure.

MulEquiv.coe_prodComm theorem

: ⇑(prodComm : M × N ≃* N × M) = Prod.swap

Full source

@[to_additive (attr := simp) coe_prodComm]
theorem coe_prodComm : ⇑(prodComm : M × NM × N ≃* N × M) = Prod.swap :=
  rfl

Component-Swapping Multiplicative Equivalence is Swap Function

Informal description

The underlying function of the multiplicative equivalence between $M \times N$ and $N \times M$ that swaps the components is equal to the swap function $\text{Prod.swap}$, which maps $(x, y)$ to $(y, x)$.

MulEquiv.coe_prodComm_symm theorem

: ⇑(prodComm : M × N ≃* N × M).symm = Prod.swap

Full source

@[to_additive (attr := simp) coe_prodComm_symm]
theorem coe_prodComm_symm : ⇑(prodComm : M × NM × N ≃* N × M).symm = Prod.swap :=
  rfl

Inverse of Component-Swapping Multiplicative Equivalence is Swap Function

Informal description

The underlying function of the inverse of the multiplicative equivalence $\text{prodComm} : M \times N \simeq^* N \times M$ is equal to the component-swapping function $\text{Prod.swap}$.

MulEquiv.prodAssoc definition

: (M × N) × P ≃* M × (N × P)

Full source

/-- The equivalence between `(M × N) × P` and `M × (N × P)` is multiplicative. -/
@[to_additive prodAssoc
      "The equivalence between `(M × N) × P` and `M × (N × P)` is additive."]
def prodAssoc : (M × N) × P(M × N) × P ≃* M × (N × P) :=
  { Equiv.prodAssoc M N P with map_mul' := fun ⟨_, _⟩ ⟨_, _⟩ => rfl }

Associativity of product monoids

Informal description

The equivalence between $(M \times N) \times P$ and $M \times (N \times P)$ is multiplicative, meaning it preserves the multiplication operation. Specifically, the map sends $((x, y), z)$ to $(x, (y, z))$ and respects the product structure.

MulEquiv.coe_prodAssoc theorem

: ⇑(prodAssoc : (M × N) × P ≃* M × (N × P)) = Equiv.prodAssoc M N P

Full source

@[to_additive (attr := simp) coe_prodAssoc]
theorem coe_prodAssoc : ⇑(prodAssoc : (M × N) × P(M × N) × P ≃* M × (N × P)) = Equiv.prodAssoc M N P :=
  rfl

Underlying Function of Associative Product Equivalence

Informal description

The underlying function of the multiplicative equivalence $\text{prodAssoc} : (M \times N) \times P \simeq^* M \times (N \times P)$ is equal to the equivalence $\text{Equiv.prodAssoc} M N P$ that associates the products $(M \times N) \times P$ and $M \times (N \times P)$.

MulEquiv.coe_prodAssoc_symm theorem

: ⇑(prodAssoc : (M × N) × P ≃* M × (N × P)).symm = (Equiv.prodAssoc M N P).symm

Full source

@[to_additive (attr := simp) coe_prodAssoc_symm]
theorem coe_prodAssoc_symm :
    ⇑(prodAssoc : (M × N) × P(M × N) × P ≃* M × (N × P)).symm = (Equiv.prodAssoc M N P).symm :=
  rfl

Inverse of Associative Product Equivalence as Function

Informal description

The underlying function of the inverse of the multiplicative equivalence $\text{prodAssoc} : (M \times N) \times P \simeq^* M \times (N \times P)$ is equal to the inverse of the equivalence $\text{Equiv.prodAssoc} M N P$.

MulEquiv.prodProdProdComm definition

: (M × N) × M' × N' ≃* (M × M') × N × N'

Full source

/-- Four-way commutativity of `Prod`. The name matches `mul_mul_mul_comm`. -/
@[to_additive (attr := simps apply) prodProdProdComm
    "Four-way commutativity of `Prod`.\nThe name matches `mul_mul_mul_comm`"]
def prodProdProdComm : (M × N) × M' × N'(M × N) × M' × N' ≃* (M × M') × N × N' :=
  { Equiv.prodProdProdComm M N M' N' with
    toFun := fun mnmn => ((mnmn.1.1, mnmn.2.1), (mnmn.1.2, mnmn.2.2))
    invFun := fun mmnn => ((mmnn.1.1, mmnn.2.1), (mmnn.1.2, mmnn.2.2))
    map_mul' := fun _mnmn _mnmn' => rfl }

Four-way product commutativity equivalence

Informal description

The multiplicative equivalence between the products $(M \times N) \times (M' \times N')$ and $(M \times M') \times (N \times N')$, which rearranges the components as $((m, n), (m', n')) \mapsto ((m, m'), (n, n'))$. This equivalence preserves the multiplicative structure.

MulEquiv.prodProdProdComm_toEquiv theorem

: (prodProdProdComm M N M' N' : _ ≃ _) = Equiv.prodProdProdComm M N M' N'

Full source

@[to_additive (attr := simp) prodProdProdComm_toEquiv]
theorem prodProdProdComm_toEquiv :
    (prodProdProdComm M N M' N' : _ ≃ _) = Equiv.prodProdProdComm M N M' N' :=
  rfl

Equivalence of Four-Way Product Commutativity

Informal description

The underlying equivalence of the multiplicative equivalence `prodProdProdComm` between $(M \times N) \times (M' \times N')$ and $(M \times M') \times (N \times N')$ is equal to the equivalence `Equiv.prodProdProdComm` that rearranges the components as $((m, n), (m', n')) \mapsto ((m, m'), (n, n'))$.

MulEquiv.prodProdProdComm_symm theorem

: (prodProdProdComm M N M' N').symm = prodProdProdComm M M' N N'

Full source

@[simp]
theorem prodProdProdComm_symm : (prodProdProdComm M N M' N').symm = prodProdProdComm M M' N N' :=
  rfl

Inverse of Four-way Product Commutativity Equivalence

Informal description

The inverse of the multiplicative equivalence `prodProdProdComm` between $(M \times N) \times (M' \times N')$ and $(M \times M') \times (N \times N')$ is itself a multiplicative equivalence of the form `prodProdProdComm M M' N N'`.

MulEquiv.prodCongr definition

(f : M ≃* M') (g : N ≃* N') : M × N ≃* M' × N'

Full source

/-- Product of multiplicative isomorphisms; the maps come from `Equiv.prodCongr`. -/
@[to_additive prodCongr "Product of additive isomorphisms; the maps come from `Equiv.prodCongr`."]
def prodCongr (f : M ≃* M') (g : N ≃* N') : M × NM × N ≃* M' × N' :=
  { f.toEquiv.prodCongr g.toEquiv with
    map_mul' := fun _ _ => Prod.ext (map_mul f _ _) (map_mul g _ _) }

Product of multiplicative equivalences

Informal description

Given multiplicative equivalences $ f : M \simeq^* M' $ and $ g : N \simeq^* N' $, the function `MulEquiv.prodCongr` constructs a multiplicative equivalence $ M \times N \simeq^* M' \times N' $ by applying $ f $ to the first component and $ g $ to the second component. This equivalence preserves the multiplication operation, meaning that for any $ (x_1, y_1), (x_2, y_2) \in M \times N $, the image of their product under the equivalence is equal to the product of their images.

MulEquiv.uniqueProd definition

[Unique N] : N × M ≃* M

Full source

/-- Multiplying by the trivial monoid doesn't change the structure. -/
@[to_additive uniqueProd "Multiplying by the trivial monoid doesn't change the structure."]
def uniqueProd [Unique N] : N × MN × M ≃* M :=
  { Equiv.uniqueProd M N with map_mul' := fun _ _ => rfl }

Isomorphism between product monoid with unique type and its second component

Informal description

Given a unique element type `N`, the product monoid `N × M` is isomorphic to `M` via the projection to the second component. The isomorphism preserves the multiplication operation.

MulEquiv.prodUnique definition

[Unique N] : M × N ≃* M

Full source

/-- Multiplying by the trivial monoid doesn't change the structure. -/
@[to_additive prodUnique "Multiplying by the trivial monoid doesn't change the structure."]
def prodUnique [Unique N] : M × NM × N ≃* M :=
  { Equiv.prodUnique M N with map_mul' := fun _ _ => rfl }

Multiplicative equivalence between product monoid and first component when second component is unique

Informal description

Given a unique element type $N$, the multiplicative equivalence between the product monoid $M \times N$ and $M$ is defined by projecting onto the first component. This equivalence preserves the multiplication operation.

MulEquiv.prodUnits definition

: (M × N)ˣ ≃* Mˣ × Nˣ

Full source

/-- The monoid equivalence between units of a product of two monoids, and the product of the
    units of each monoid. -/
@[to_additive prodAddUnits
      "The additive monoid equivalence between additive units of a product
      of two additive monoids, and the product of the additive units of each additive monoid."]
def prodUnits : (M × N)ˣ(M × N)ˣ ≃* Mˣ × Nˣ where
  toFun := (Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N))
  invFun u := ⟨(u.1, u.2), (↑u.1⁻¹, ↑u.2⁻¹), by simp, by simp⟩
  left_inv u := by
    simp only [MonoidHom.prod_apply, Units.coe_map, MonoidHom.coe_fst, MonoidHom.coe_snd,
      Prod.mk.eta, Units.coe_map_inv, Units.mk_val]
  right_inv := fun ⟨u₁, u₂⟩ => by
    simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv,
      MonoidHom.coe_snd, MonoidHom.prod_apply, Prod.mk.injEq]
    exact ⟨rfl, rfl⟩
  map_mul' := MonoidHom.map_mul _

Multiplicative equivalence between units of a product and product of units

Informal description

The multiplicative equivalence between the group of units of the product monoid $ M \times N $ and the product of the groups of units of $ M $ and $ N $. Specifically, it maps a unit $(x, y)$ of $ M \times N $ to the pair $(x, y)$ where $ x $ is a unit of $ M $ and $ y $ is a unit of $ N $, and its inverse maps a pair of units $(u, v)$ to the unit $(u, v)$ of $ M \times N $. This equivalence preserves the multiplication operation.

Prod.isUnit_iff theorem

{x : M × N} : IsUnit x ↔ IsUnit x.1 ∧ IsUnit x.2

Full source

@[to_additive]
lemma _root_.Prod.isUnit_iff {x : M × N} : IsUnitIsUnit x ↔ IsUnit x.1 ∧ IsUnit x.2 where
  mp h := ⟨(prodUnits h.unit).1.isUnit, (prodUnits h.unit).2.isUnit⟩
  mpr h := (prodUnits.symm (h.1.unit, h.2.unit)).isUnit

Characterization of Units in Product Monoid: $(x_1, x_2)$ is a unit iff $x_1$ and $x_2$ are units

Informal description

An element $x = (x_1, x_2)$ of the product monoid $M \times N$ is a unit if and only if both components $x_1$ and $x_2$ are units in their respective monoids $M$ and $N$.

Units.embedProduct definition

(α : Type*) [Monoid α] : αˣ →* α × αᵐᵒᵖ

Full source

/-- Canonical homomorphism of monoids from `αˣ` into `α × αᵐᵒᵖ`.
Used mainly to define the natural topology of `αˣ`. -/
@[to_additive (attr := simps)
      "Canonical homomorphism of additive monoids from `AddUnits α` into `α × αᵃᵒᵖ`.
      Used mainly to define the natural topology of `AddUnits α`."]
def embedProduct (α : Type*) [Monoid α] : αˣαˣ →* α × αᵐᵒᵖ where
  toFun x := ⟨x, op ↑x⁻¹⟩
  map_one' := by
    simp only [inv_one, eq_self_iff_true, Units.val_one, op_one, Prod.mk_eq_one, and_self_iff]
  map_mul' x y := by simp only [mul_inv_rev, op_mul, Units.val_mul, Prod.mk_mul_mk]

Canonical homomorphism from units to $\alpha \times \alpha^{\mathrm{op}}$

Informal description

The canonical homomorphism from the group of units $\alpha^\times$ of a monoid $\alpha$ into the product $\alpha \times \alpha^{\mathrm{op}}$, where $\alpha^{\mathrm{op}}$ is the opposite monoid. Specifically, it maps each unit $x \in \alpha^\times$ to the pair $(x, x^{-1})$ (with $x^{-1}$ considered in the opposite monoid). This homomorphism is primarily used to define the natural topology on $\alpha^\times$.

Units.embedProduct_injective theorem

(α : Type*) [Monoid α] : Function.Injective (embedProduct α)

Full source

@[to_additive]
theorem embedProduct_injective (α : Type*) [Monoid α] : Function.Injective (embedProduct α) :=
  fun _ _ h => Units.ext <| (congr_arg Prod.fst h :)

Injectivity of the canonical homomorphism from units to $\alpha \times \alpha^{\mathrm{op}}$

Informal description

For any monoid $\alpha$, the canonical homomorphism $\alpha^\times \to \alpha \times \alpha^{\mathrm{op}}$ that maps each unit $x \in \alpha^\times$ to $(x, x^{-1})$ is injective.

mulMulHom definition

[CommSemigroup α] : α × α →ₙ* α

Full source

/-- Multiplication as a multiplicative homomorphism. -/
@[to_additive (attr := simps) "Addition as an additive homomorphism."]
def mulMulHom [CommSemigroup α] :
    α × αα × α →ₙ* α where
  toFun a := a.1 * a.2
  map_mul' _ _ := mul_mul_mul_comm _ _ _ _

Multiplication as a multiplicative homomorphism

Informal description

The function that takes a pair $(a, b)$ in a commutative semigroup $\alpha$ and returns their product $a \cdot b$, viewed as a multiplicative homomorphism.

mulMonoidHom definition

[CommMonoid α] : α × α →* α

Full source

/-- Multiplication as a monoid homomorphism. -/
@[to_additive (attr := simps) "Addition as an additive monoid homomorphism."]
def mulMonoidHom [CommMonoid α] : α × αα × α →* α :=
  { mulMulHom with map_one' := mul_one _ }

Multiplication as a monoid homomorphism

Informal description

The function that takes a pair $(a, b)$ in a commutative monoid $\alpha$ and returns their product $a \cdot b$, viewed as a monoid homomorphism. This extends the multiplicative homomorphism version (`mulMulHom`) by additionally preserving the multiplicative identity (i.e., $(1,1) \mapsto 1$).

divMonoidHom definition

[DivisionCommMonoid α] : α × α →* α

Full source

/-- Division as a monoid homomorphism. -/
@[to_additive (attr := simps) "Subtraction as an additive monoid homomorphism."]
def divMonoidHom [DivisionCommMonoid α] : α × αα × α →* α where
  toFun a := a.1 / a.2
  map_one' := div_one _
  map_mul' _ _ := mul_div_mul_comm _ _ _ _

Division as a monoid homomorphism

Informal description

The function that takes a pair $(a, b)$ in a commutative division monoid $\alpha$ and returns their quotient $a / b$, viewed as a monoid homomorphism.

Main declarations