------------------------------------------------------------------------ -- The Agda standard library -- -- Some theory for commutative semigroup ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Bundles using (CommutativeSemigroup) module Algebra.Properties.CommutativeSemigroup {a ℓ} (CS : CommutativeSemigroup a ℓ) where open CommutativeSemigroup CS open import Algebra.Definitions _≈_ open import Relation.Binary.Reasoning.Setoid setoid open import Data.Product.Base using (_,_) ------------------------------------------------------------------------ -- Re-export the contents of semigroup open import Algebra.Properties.Semigroup semigroup public ------------------------------------------------------------------------ -- Properties interchange : Interchangable _∙_ _∙_ interchange a b c d = begin (a ∙ b) ∙ (c ∙ d) ≈⟨ assoc a b (c ∙ d) ⟩ a ∙ (b ∙ (c ∙ d)) ≈⟨ ∙-congˡ (assoc b c d) ⟨ a ∙ ((b ∙ c) ∙ d) ≈⟨ ∙-congˡ (∙-congʳ (comm b c)) ⟩ a ∙ ((c ∙ b) ∙ d) ≈⟨ ∙-congˡ (assoc c b d) ⟩ a ∙ (c ∙ (b ∙ d)) ≈⟨ assoc a c (b ∙ d) ⟨ (a ∙ c) ∙ (b ∙ d) ∎ ------------------------------------------------------------------------ -- Permutation laws for _∙_ for three factors. -- There are five nontrivial permutations. ------------------------------------------------------------------------ -- Partitions (1,1). x∙yz≈y∙xz : ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (x ∙ z) x∙yz≈y∙xz x y z = begin x ∙ (y ∙ z) ≈⟨ sym (assoc x y z) ⟩ (x ∙ y) ∙ z ≈⟨ ∙-congʳ (comm x y) ⟩ (y ∙ x) ∙ z ≈⟨ assoc y x z ⟩ y ∙ (x ∙ z) ∎ x∙yz≈z∙yx : ∀ x y z → x ∙ (y ∙ z) ≈ z ∙ (y ∙ x) x∙yz≈z∙yx x y z = begin x ∙ (y ∙ z) ≈⟨ ∙-congˡ (comm y z) ⟩ x ∙ (z ∙ y) ≈⟨ x∙yz≈y∙xz x z y ⟩ z ∙ (x ∙ y) ≈⟨ ∙-congˡ (comm x y) ⟩ z ∙ (y ∙ x) ∎ x∙yz≈x∙zy : ∀ x y z → x ∙ (y ∙ z) ≈ x ∙ (z ∙ y) x∙yz≈x∙zy _ y z = ∙-congˡ (comm y z) x∙yz≈y∙zx : ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (z ∙ x) x∙yz≈y∙zx x y z = begin x ∙ (y ∙ z) ≈⟨ comm x _ ⟩ (y ∙ z) ∙ x ≈⟨ assoc y z x ⟩ y ∙ (z ∙ x) ∎ x∙yz≈z∙xy : ∀ x y z → x ∙ (y ∙ z) ≈ z ∙ (x ∙ y) x∙yz≈z∙xy x y z = begin x ∙ (y ∙ z) ≈⟨ sym (assoc x y z) ⟩ (x ∙ y) ∙ z ≈⟨ comm _ z ⟩ z ∙ (x ∙ y) ∎ ------------------------------------------------------------------------ -- Partitions (1,2). -- These permutation laws are proved by composing the proofs for -- partitions (1,1) with \p → trans p (sym (assoc _ _ _)). x∙yz≈yx∙z : ∀ x y z → x ∙ (y ∙ z) ≈ (y ∙ x) ∙ z x∙yz≈yx∙z x y z = trans (x∙yz≈y∙xz x y z) (sym (assoc y x z)) x∙yz≈zy∙x : ∀ x y z → x ∙ (y ∙ z) ≈ (z ∙ y) ∙ x x∙yz≈zy∙x x y z = trans (x∙yz≈z∙yx x y z) (sym (assoc z y x)) x∙yz≈xz∙y : ∀ x y z → x ∙ (y ∙ z) ≈ (x ∙ z) ∙ y x∙yz≈xz∙y x y z = trans (x∙yz≈x∙zy x y z) (sym (assoc x z y)) x∙yz≈yz∙x : ∀ x y z → x ∙ (y ∙ z) ≈ (y ∙ z) ∙ x x∙yz≈yz∙x x y z = trans (x∙yz≈y∙zx _ _ _) (sym (assoc y z x)) x∙yz≈zx∙y : ∀ x y z → x ∙ (y ∙ z) ≈ (z ∙ x) ∙ y x∙yz≈zx∙y x y z = trans (x∙yz≈z∙xy x y z) (sym (assoc z x y)) ------------------------------------------------------------------------ -- Partitions (2,1). -- Their laws are proved by composing proofs for partitions (1,1) with -- trans (assoc x y z). xy∙z≈y∙xz : ∀ x y z → (x ∙ y) ∙ z ≈ y ∙ (x ∙ z) xy∙z≈y∙xz x y z = trans (assoc x y z) (x∙yz≈y∙xz x y z) xy∙z≈z∙yx : ∀ x y z → (x ∙ y) ∙ z ≈ z ∙ (y ∙ x) xy∙z≈z∙yx x y z = trans (assoc x y z) (x∙yz≈z∙yx x y z) xy∙z≈x∙zy : ∀ x y z → (x ∙ y) ∙ z ≈ x ∙ (z ∙ y) xy∙z≈x∙zy x y z = trans (assoc x y z) (x∙yz≈x∙zy x y z) xy∙z≈y∙zx : ∀ x y z → (x ∙ y) ∙ z ≈ y ∙ (z ∙ x) xy∙z≈y∙zx x y z = trans (assoc x y z) (x∙yz≈y∙zx x y z) xy∙z≈z∙xy : ∀ x y z → (x ∙ y) ∙ z ≈ z ∙ (x ∙ y) xy∙z≈z∙xy x y z = trans (assoc x y z) (x∙yz≈z∙xy x y z) ------------------------------------------------------------------------ -- Partitions (2,2). -- These proofs are by composing with the proofs for (2,1). xy∙z≈yx∙z : ∀ x y z → (x ∙ y) ∙ z ≈ (y ∙ x) ∙ z xy∙z≈yx∙z x y z = trans (xy∙z≈y∙xz _ _ _) (sym (assoc y x z)) xy∙z≈zy∙x : ∀ x y z → (x ∙ y) ∙ z ≈ (z ∙ y) ∙ x xy∙z≈zy∙x x y z = trans (xy∙z≈z∙yx x y z) (sym (assoc z y x)) xy∙z≈xz∙y : ∀ x y z → (x ∙ y) ∙ z ≈ (x ∙ z) ∙ y xy∙z≈xz∙y x y z = trans (xy∙z≈x∙zy x y z) (sym (assoc x z y)) xy∙z≈yz∙x : ∀ x y z → (x ∙ y) ∙ z ≈ (y ∙ z) ∙ x xy∙z≈yz∙x x y z = trans (xy∙z≈y∙zx x y z) (sym (assoc y z x)) xy∙z≈zx∙y : ∀ x y z → (x ∙ y) ∙ z ≈ (z ∙ x) ∙ y xy∙z≈zx∙y x y z = trans (xy∙z≈z∙xy x y z) (sym (assoc z x y)) ------------------------------------------------------------------------ -- commutative semigroup has Jordan identity xy∙xx≈x∙yxx : ∀ x y → (x ∙ y) ∙ (x ∙ x) ≈ x ∙ (y ∙ (x ∙ x)) xy∙xx≈x∙yxx x y = assoc x y ((x ∙ x)) ------------------------------------------------------------------------ -- commutative semigroup is left/right/middle semiMedial semimedialˡ : LeftSemimedial _∙_ semimedialˡ x y z = begin (x ∙ x) ∙ (y ∙ z) ≈⟨ assoc x x (y ∙ z) ⟩ x ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (sym (assoc x y z)) ⟩ x ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩ x ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩ x ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc x y ((x ∙ z))) ⟩ (x ∙ y) ∙ (x ∙ z) ∎ semimedialʳ : RightSemimedial _∙_ semimedialʳ x y z = begin (y ∙ z) ∙ (x ∙ x) ≈⟨ assoc y z (x ∙ x) ⟩ y ∙ (z ∙ (x ∙ x)) ≈⟨ ∙-congˡ (sym (assoc z x x)) ⟩ y ∙ ((z ∙ x) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (comm z x)) ⟩ y ∙ ((x ∙ z) ∙ x) ≈⟨ ∙-congˡ (assoc x z x) ⟩ y ∙ (x ∙ (z ∙ x)) ≈⟨ sym (assoc y x ((z ∙ x))) ⟩ (y ∙ x) ∙ (z ∙ x) ∎ middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x) middleSemimedial x y z = begin (x ∙ y) ∙ (z ∙ x) ≈⟨ assoc x y ((z ∙ x)) ⟩ x ∙ (y ∙ (z ∙ x)) ≈⟨ ∙-congˡ (sym (assoc y z x)) ⟩ x ∙ ((y ∙ z) ∙ x) ≈⟨ ∙-congˡ (∙-congʳ (comm y z)) ⟩ x ∙ ((z ∙ y) ∙ x) ≈⟨ ∙-congˡ ( assoc z y x) ⟩ x ∙ (z ∙ (y ∙ x)) ≈⟨ sym (assoc x z ((y ∙ x))) ⟩ (x ∙ z) ∙ (y ∙ x) ∎ semimedial : Semimedial _∙_ semimedial = semimedialˡ , semimedialʳ