Order homomorphisms for products of linearly ordered groups with zero

This file defines order homomorphisms for products of linearly ordered groups with zero, which is identified with the WithZero of the lexicographic product of the units of the groups.

The product of linearly ordered groups with zero WithZero (αˣ ×ₗ βˣ) is a linearly ordered group with zero itself with natural inclusions but only one projection. One has to work with the lexicographic product of the units αˣ ×ₗ βˣ since otherwise, the plain product αˣ × βˣ would not be linearly ordered.

TODO

Create the "LinOrdCommGrpWithZero" category.

def toLexMulEquiv (G : Type u_1) (H : Type u_2) [MulOneClass G] [MulOneClass H] : G × H ≃* Lex (G × H)

toLex as a monoid isomorphism.

Equations

• toLexMulEquiv G H = { toFun := ⇑toLex, invFun := ⇑ofLex, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem coe_toLexMulEquiv (G : Type u_1) (H : Type u_2) [MulOneClass G] [MulOneClass H] : ⇑(toLexMulEquiv G H) = ⇑toLex

@[simp]

theorem coe_symm_toLexMulEquiv (G : Type u_1) (H : Type u_2) [MulOneClass G] [MulOneClass H] : ⇑(toLexMulEquiv G H).symm = ⇑ofLex

@[simp]

theorem toEquiv_toLexMulEquiv (G : Type u_1) (H : Type u_2) [MulOneClass G] [MulOneClass H] : ⇑↑(toLexMulEquiv G H) = ⇑toLex

@[simp]

theorem toEquiv_symm_toLexMulEquiv (G : Type u_1) (H : Type u_2) [MulOneClass G] [MulOneClass H] : ⇑↑(toLexMulEquiv G H).symm = ⇑ofLex

theorem MonoidWithZeroHom.inl_mono {M₀ : Type u_1} {N₀ : Type u_2} [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [Preorder N₀] [DecidablePred fun (x : M₀) => x = 0] : Monotone ⇑(inl M₀ N₀)

theorem MonoidWithZeroHom.inl_strictMono {M₀ : Type u_1} {N₀ : Type u_2} [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [PartialOrder N₀] [DecidablePred fun (x : M₀) => x = 0] : StrictMono ⇑(inl M₀ N₀)

theorem MonoidWithZeroHom.inr_mono {M₀ : Type u_1} {N₀ : Type u_2} [GroupWithZero M₀] [Preorder M₀] [LinearOrderedCommGroupWithZero N₀] [DecidablePred fun (x : N₀) => x = 0] : Monotone ⇑(inr M₀ N₀)

theorem MonoidWithZeroHom.inr_strictMono {M₀ : Type u_1} {N₀ : Type u_2} [GroupWithZero M₀] [PartialOrder M₀] [LinearOrderedCommGroupWithZero N₀] [DecidablePred fun (x : N₀) => x = 0] : StrictMono ⇑(inr M₀ N₀)

theorem MonoidWithZeroHom.fst_mono {M₀ : Type u_1} {N₀ : Type u_2} [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [Preorder N₀] : Monotone ⇑(fst M₀ N₀)

theorem MonoidWithZeroHom.snd_mono {M₀ : Type u_1} {N₀ : Type u_2} [GroupWithZero M₀] [Preorder M₀] [LinearOrderedCommGroupWithZero N₀] : Monotone ⇑(snd M₀ N₀)

def LinearOrderedCommGroupWithZero.inl (α : Type u_1) (β : Type u_2) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] : α →*₀o WithZero (Lex (αˣ × βˣ))

Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from M to WithZero (Mˣ ×ₗ Nˣ), which is the linearly ordered group with zero that can be identified as their product.

Equations

• LinearOrderedCommGroupWithZero.inl α β = { toMonoidWithZeroHom := (WithZero.map' (toLexMulEquiv αˣ βˣ).toMonoidHom).comp (MonoidWithZeroHom.inl α β), monotone' := ⋯ }

@[simp]

theorem LinearOrderedCommGroupWithZero.inl_apply (α : Type u_1) (β : Type u_2) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] (a✝ : α) : (inl α β) a✝ = (WithZero.map' ↑(toLexMulEquiv αˣ βˣ)) ((MonoidWithZeroHom.inl α β) a✝)

def LinearOrderedCommGroupWithZero.inr (α : Type u_1) (β : Type u_2) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] : β →*₀o WithZero (Lex (αˣ × βˣ))

Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from N to WithZero (Mˣ ×ₗ Nˣ), which is the linearly ordered group with zero that can be identified as their product.

Equations

• LinearOrderedCommGroupWithZero.inr α β = { toMonoidWithZeroHom := (WithZero.map' (toLexMulEquiv αˣ βˣ).toMonoidHom).comp (MonoidWithZeroHom.inr α β), monotone' := ⋯ }

@[simp]

theorem LinearOrderedCommGroupWithZero.inr_apply (α : Type u_1) (β : Type u_2) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] (a✝ : β) : (inr α β) a✝ = (WithZero.map' ↑(toLexMulEquiv αˣ βˣ)) ((MonoidWithZeroHom.inr α β) a✝)

def LinearOrderedCommGroupWithZero.fst (α : Type u_1) (β : Type u_2) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] : WithZero (Lex (αˣ × βˣ)) →*₀o α

Given linearly ordered groups with zero M, N, the natural projection ordered homomorphism from WithZero (Mˣ ×ₗ Nˣ) to M, which is the linearly ordered group with zero that can be identified as their product.

Equations

• LinearOrderedCommGroupWithZero.fst α β = { toMonoidWithZeroHom := (MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv αˣ βˣ).symm.toMonoidHom), monotone' := ⋯ }

@[simp]

theorem LinearOrderedCommGroupWithZero.fst_apply (α : Type u_1) (β : Type u_2) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] (a✝ : WithZero (Lex (αˣ × βˣ))) : (fst α β) a✝ = (MonoidWithZeroHom.fst α β) ((WithZero.map' ↑(toLexMulEquiv αˣ βˣ).symm) a✝)

@[simp]

theorem LinearOrderedCommGroupWithZero.fst_comp_inl (α : Type u_1) (β : Type u_2) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] : (fst α β).comp (inl α β) = OrderMonoidWithZeroHom.id α

theorem LinearOrderedCommGroupWithZero.inl_eq_coe_inlₗ {α : Type u_1} {β : Type u_2} [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] {m : α} (hm : m ≠ 0) : (inl α β) m = ↑((OrderMonoidHom.inlₗ αˣ βˣ) (Units.mk0 m hm))

theorem LinearOrderedCommGroupWithZero.inr_eq_coe_inrₗ {α : Type u_1} {β : Type u_2} [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] {n : β} (hn : n ≠ 0) : (inr α β) n = ↑((OrderMonoidHom.inrₗ αˣ βˣ) (Units.mk0 n hn))

theorem LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex {α : Type u_1} {β : Type u_2} [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β] {m : α} {n : β} (hm : m ≠ 0) (hn : n ≠ 0) : (inl α β) m * (inr α β) n = ↑(toLex (Units.mk0 m hm, Units.mk0 n hn))