Order homomorphisms for products of ordered monoids

This file defines order homomorphisms for products of ordered monoids, for both the plain product and the lexicographic product.

The product of ordered monoids α × β is an ordered monoid itself with both natural inclusions and projections, making it the coproduct as well.

TODO

Create the "OrdCommMon" category.

theorem MonoidHom.inl_mono {α : Type u_1} {β : Type u_2} [Monoid α] [Preorder α] [Monoid β] [Preorder β] : Monotone ⇑(inl α β)

theorem AddMonoidHom.inl_mono {α : Type u_1} {β : Type u_2} [AddMonoid α] [Preorder α] [AddMonoid β] [Preorder β] : Monotone ⇑(inl α β)

theorem MonoidHom.inl_strictMono {α : Type u_1} {β : Type u_2} [Monoid α] [Preorder α] [Monoid β] [Preorder β] : StrictMono ⇑(inl α β)

theorem AddMonoidHom.inl_strictMono {α : Type u_1} {β : Type u_2} [AddMonoid α] [Preorder α] [AddMonoid β] [Preorder β] : StrictMono ⇑(inl α β)

theorem MonoidHom.inr_mono {α : Type u_1} {β : Type u_2} [Monoid α] [Preorder α] [Monoid β] [Preorder β] : Monotone ⇑(inr α β)

theorem AddMonoidHom.inr_mono {α : Type u_1} {β : Type u_2} [AddMonoid α] [Preorder α] [AddMonoid β] [Preorder β] : Monotone ⇑(inr α β)

theorem MonoidHom.inr_strictMono {α : Type u_1} {β : Type u_2} [Monoid α] [Preorder α] [Monoid β] [Preorder β] : StrictMono ⇑(inr α β)

theorem AddMonoidHom.inr_strictMono {α : Type u_1} {β : Type u_2} [AddMonoid α] [Preorder α] [AddMonoid β] [Preorder β] : StrictMono ⇑(inr α β)

theorem MonoidHom.fst_mono {α : Type u_1} {β : Type u_2} [Monoid α] [Preorder α] [Monoid β] [Preorder β] : Monotone ⇑(fst α β)

theorem AddMonoidHom.fst_mono {α : Type u_1} {β : Type u_2} [AddMonoid α] [Preorder α] [AddMonoid β] [Preorder β] : Monotone ⇑(fst α β)

theorem MonoidHom.snd_mono {α : Type u_1} {β : Type u_2} [Monoid α] [Preorder α] [Monoid β] [Preorder β] : Monotone ⇑(snd α β)

theorem AddMonoidHom.snd_mono {α : Type u_1} {β : Type u_2} [AddMonoid α] [Preorder α] [AddMonoid β] [Preorder β] : Monotone ⇑(snd α β)

def OrderMonoidHom.inl (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : α →*o α × β

Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to M × N.

Equations

• OrderMonoidHom.inl α β = { toMonoidHom := MonoidHom.inl α β, monotone' := ⋯ }

def OrderAddMonoidHom.inl (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : α →+o α × β

Given ordered additive monoids M, N, the natural inclusion ordered homomorphism from M to M × N.

Equations

• OrderAddMonoidHom.inl α β = { toAddMonoidHom := AddMonoidHom.inl α β, monotone' := ⋯ }

@[simp]

theorem OrderAddMonoidHom.inl_apply (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (x : α) : (inl α β) x = (x, 0)

@[simp]

theorem OrderMonoidHom.inl_apply (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (x : α) : (inl α β) x = (x, 1)

def OrderMonoidHom.inr (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : β →*o α × β

Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to M × N.

Equations

• OrderMonoidHom.inr α β = { toMonoidHom := MonoidHom.inr α β, monotone' := ⋯ }

def OrderAddMonoidHom.inr (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : β →+o α × β

Given ordered additive monoids M, N, the natural inclusion ordered homomorphism from N to M × N.

Equations

• OrderAddMonoidHom.inr α β = { toAddMonoidHom := AddMonoidHom.inr α β, monotone' := ⋯ }

@[simp]

theorem OrderAddMonoidHom.inr_apply (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (y : β) : (inr α β) y = (0, y)

@[simp]

theorem OrderMonoidHom.inr_apply (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (y : β) : (inr α β) y = (1, y)

def OrderMonoidHom.fst (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : α × β →*o α

Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to M.

Equations

• OrderMonoidHom.fst α β = { toMonoidHom := MonoidHom.fst α β, monotone' := ⋯ }

def OrderAddMonoidHom.fst (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : α × β →+o α

Given ordered additive monoids M, N, the natural projection ordered homomorphism from M × N to M.

Equations

• OrderAddMonoidHom.fst α β = { toAddMonoidHom := AddMonoidHom.fst α β, monotone' := ⋯ }

@[simp]

theorem OrderMonoidHom.fst_apply (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (self : α × β) : (fst α β) self = self.1

@[simp]

theorem OrderAddMonoidHom.fst_apply (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (self : α × β) : (fst α β) self = self.1

def OrderMonoidHom.snd (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : α × β →*o β

Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to N.

Equations

• OrderMonoidHom.snd α β = { toMonoidHom := MonoidHom.snd α β, monotone' := ⋯ }

def OrderAddMonoidHom.snd (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : α × β →+o β

Given ordered additive monoids M, N, the natural projection ordered homomorphism from M × N to N.

Equations

• OrderAddMonoidHom.snd α β = { toAddMonoidHom := AddMonoidHom.snd α β, monotone' := ⋯ }

@[simp]

theorem OrderMonoidHom.snd_apply (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (self : α × β) : (snd α β) self = self.2

@[simp]

theorem OrderAddMonoidHom.snd_apply (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (self : α × β) : (snd α β) self = self.2

def OrderMonoidHom.inlₗ (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : α →*o Lex (α × β)

Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to the lexicographic M ×ₗ N.

Equations

• OrderMonoidHom.inlₗ α β = { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderMonoidHom.inl α β)).toFun, map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }

def OrderAddMonoidHom.inlₗ (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : α →+o Lex (α × β)

Given ordered additive monoids M, N, the natural inclusion ordered homomorphism from M to the lexicographic M ×ₗ N.

Equations

• OrderAddMonoidHom.inlₗ α β = { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderAddMonoidHom.inl α β)).toFun, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }

@[simp]

theorem OrderAddMonoidHom.inlₗ_apply (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (a✝ : α) : (inlₗ α β) a✝ = toLex (a✝, 0)

@[simp]

theorem OrderMonoidHom.inlₗ_apply (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (a✝ : α) : (inlₗ α β) a✝ = toLex (a✝, 1)

def OrderMonoidHom.inrₗ (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : β →*o Lex (α × β)

Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to the lexicographic M ×ₗ N.

Equations

• OrderMonoidHom.inrₗ α β = { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderMonoidHom.inr α β)).toFun, map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }

def OrderAddMonoidHom.inrₗ (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : β →+o Lex (α × β)

Given ordered additive monoids M, N, the natural inclusion ordered homomorphism from N to the lexicographic M ×ₗ N.

Equations

• OrderAddMonoidHom.inrₗ α β = { toFun := (Prod.Lex.toLexOrderHom.comp ↑(OrderAddMonoidHom.inr α β)).toFun, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }

@[simp]

theorem OrderAddMonoidHom.inrₗ_apply (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (a✝ : β) : (inrₗ α β) a✝ = toLex (0, a✝)

@[simp]

theorem OrderMonoidHom.inrₗ_apply (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (a✝ : β) : (inrₗ α β) a✝ = toLex (1, a✝)

def OrderMonoidHom.fstₗ (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : Lex (α × β) →*o α

Given ordered monoids M, N, the natural projection ordered homomorphism from the lexicographic M ×ₗ N to M.

Equations

• OrderMonoidHom.fstₗ α β = { toFun := fun (p : Lex (α × β)) => (ofLex p).1, map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }

def OrderAddMonoidHom.fstₗ (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : Lex (α × β) →+o α

Given ordered additive monoids M, N, the natural projection ordered homomorphism from the lexicographic M ×ₗ N to M.

Equations

• OrderAddMonoidHom.fstₗ α β = { toFun := fun (p : Lex (α × β)) => (ofLex p).1, map_zero' := ⋯, map_add' := ⋯, monotone' := ⋯ }

@[simp]

theorem OrderMonoidHom.fstₗ_apply (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (p : Lex (α × β)) : (fstₗ α β) p = (ofLex p).1

@[simp]

theorem OrderAddMonoidHom.fstₗ_apply (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (p : Lex (α × β)) : (fstₗ α β) p = (ofLex p).1

@[simp]

theorem OrderMonoidHom.fst_comp_inl (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : (fst α β).comp (inl α β) = OrderMonoidHom.id α

@[simp]

theorem OrderAddMonoidHom.fst_comp_inl (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : (fst α β).comp (inl α β) = OrderAddMonoidHom.id α

@[simp]

theorem OrderMonoidHom.fstₗ_comp_inlₗ (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : (fstₗ α β).comp (inlₗ α β) = OrderMonoidHom.id α

@[simp]

theorem OrderAddMonoidHom.fstₗ_comp_inlₗ (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : (fstₗ α β).comp (inlₗ α β) = OrderAddMonoidHom.id α

@[simp]

theorem OrderMonoidHom.snd_comp_inl (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : (snd α β).comp (inl α β) = 1

@[simp]

theorem OrderAddMonoidHom.snd_comp_inl (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : (snd α β).comp (inl α β) = 0

@[simp]

theorem OrderMonoidHom.fst_comp_inr (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : (fst α β).comp (inr α β) = 1

@[simp]

theorem OrderAddMonoidHom.fst_comp_inr (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : (fst α β).comp (inr α β) = 0

@[simp]

theorem OrderMonoidHom.snd_comp_inr (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] : (snd α β).comp (inr α β) = OrderMonoidHom.id β

@[simp]

theorem OrderAddMonoidHom.snd_comp_inr (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] : (snd α β).comp (inr α β) = OrderAddMonoidHom.id β

theorem OrderMonoidHom.inl_mul_inr_eq_mk (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (m : α) (n : β) : (inl α β) m * (inr α β) n = (m, n)

theorem OrderAddMonoidHom.inl_add_inr_eq_mk (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (m : α) (n : β) : (inl α β) m + (inr α β) n = (m, n)

theorem OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex (α : Type u_1) (β : Type u_2) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (m : α) (n : β) : (inlₗ α β) m * (inrₗ α β) n = toLex (m, n)

theorem OrderAddMonoidHom.inlₗ_add_inrₗ_eq_toLex (α : Type u_1) (β : Type u_2) [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (m : α) (n : β) : (inlₗ α β) m + (inrₗ α β) n = toLex (m, n)

theorem OrderMonoidHom.commute_inl_inr {α : Type u_1} {β : Type u_2} [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (m : α) (n : β) : Commute ((inl α β) m) ((inr α β) n)

theorem OrderAddMonoidHom.addCommute_inl_inr {α : Type u_1} {β : Type u_2} [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (m : α) (n : β) : AddCommute ((inl α β) m) ((inr α β) n)

theorem OrderMonoidHom.commute_inlₗ_inrₗ {α : Type u_1} {β : Type u_2} [Monoid α] [PartialOrder α] [Monoid β] [Preorder β] (m : α) (n : β) : Commute ((inlₗ α β) m) ((inrₗ α β) n)

theorem OrderAddMonoidHom.addCommute_inlₗ_inrₗ {α : Type u_1} {β : Type u_2} [AddMonoid α] [PartialOrder α] [AddMonoid β] [Preorder β] (m : α) (n : β) : AddCommute ((inlₗ α β) m) ((inrₗ α β) n)