------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of scaling and other operations
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Module.Consequences where
open import Algebra.Core using (Op₂)
import Algebra.Definitions as Defs
open import Algebra.Module.Core using (Opₗ; Opᵣ)
open import Algebra.Module.Definitions
open import Function.Base using (flip)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
private
variable
a b c ℓ ℓa : Level
A : Set a
B : Set b
module _ (_≈ᴬ_ : Rel {a} A ℓa) (S : Setoid c ℓ) where
open Setoid S
open ≈-Reasoning S
open Defs _≈ᴬ_
private
module L = LeftDefs A _≈_
module R = RightDefs A _≈_
module B = BiDefs A A _≈_
module _ {_*_ : Op₂ A} {_*ₗ_ : Opₗ A Carrier} where
private
_*ᵣ_ = flip _*ₗ_
*ₗ-assoc∧comm⇒*ᵣ-assoc :
L.RightCongruent _≈ᴬ_ _*ₗ_ →
L.Associative _*_ _*ₗ_ → Commutative _*_ → R.Associative _*_ _*ᵣ_
*ₗ-assoc∧comm⇒*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm m x y = begin
(m *ᵣ x) *ᵣ y ≈⟨ refl ⟩
y *ₗ (x *ₗ m) ≈⟨ *ₗ-assoc _ _ _ ⟨
(y * x) *ₗ m ≈⟨ *ₗ-congʳ (*-comm y x) ⟩
(x * y) *ₗ m ≈⟨ refl ⟩
m *ᵣ (x * y) ∎
*ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc :
L.RightCongruent _≈ᴬ_ _*ₗ_ →
L.Associative _*_ _*ₗ_ → Commutative _*_ → B.Associative _*ₗ_ _*ᵣ_
*ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm x m y = begin
((x *ₗ m) *ᵣ y) ≈⟨ refl ⟩
(y *ₗ (x *ₗ m)) ≈⟨ *ₗ-assoc _ _ _ ⟨
((y * x) *ₗ m) ≈⟨ *ₗ-congʳ (*-comm y x) ⟩
((x * y) *ₗ m) ≈⟨ *ₗ-assoc _ _ _ ⟩
(x *ₗ (y *ₗ m)) ≈⟨ refl ⟩
(x *ₗ (m *ᵣ y)) ∎
module _ {_*_ : Op₂ A} {_*ᵣ_ : Opᵣ A Carrier} where
private
_*ₗ_ = flip _*ᵣ_
*ᵣ-assoc∧comm⇒*ₗ-assoc :
R.LeftCongruent _≈ᴬ_ _*ᵣ_ →
R.Associative _*_ _*ᵣ_ → Commutative _*_ → L.Associative _*_ _*ₗ_
*ᵣ-assoc∧comm⇒*ₗ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x y m = begin
((x * y) *ₗ m) ≈⟨ refl ⟩
(m *ᵣ (x * y)) ≈⟨ *ᵣ-congˡ (*-comm x y) ⟩
(m *ᵣ (y * x)) ≈⟨ *ᵣ-assoc _ _ _ ⟨
((m *ᵣ y) *ᵣ x) ≈⟨ refl ⟩
(x *ₗ (y *ₗ m)) ∎
*ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc :
R.LeftCongruent _≈ᴬ_ _*ᵣ_ →
R.Associative _*_ _*ᵣ_ → Commutative _*_ → B.Associative _*ₗ_ _*ᵣ_
*ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x m y = begin
((x *ₗ m) *ᵣ y) ≈⟨ refl ⟩
((m *ᵣ x) *ᵣ y) ≈⟨ *ᵣ-assoc _ _ _ ⟩
(m *ᵣ (x * y)) ≈⟨ *ᵣ-congˡ (*-comm x y) ⟩
(m *ᵣ (y * x)) ≈⟨ *ᵣ-assoc _ _ _ ⟨
((m *ᵣ y) *ᵣ x) ≈⟨ refl ⟩
(x *ₗ (m *ᵣ y)) ∎
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.3
*ₗ-assoc+comm⇒*ᵣ-assoc = *ₗ-assoc∧comm⇒*ᵣ-assoc
{-# WARNING_ON_USAGE *ₗ-assoc+comm⇒*ᵣ-assoc
"Warning: *ₗ-assoc+comm⇒*ᵣ-assoc was deprecated in v2.3.
Please use *ₗ-assoc∧comm⇒*ᵣ-assoc instead."
#-}
*ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc = *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
{-# WARNING_ON_USAGE *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc
"Warning: *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc was deprecated in v2.3.
Please use *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc instead."
#-}
*ᵣ-assoc+comm⇒*ₗ-assoc = *ᵣ-assoc∧comm⇒*ₗ-assoc
{-# WARNING_ON_USAGE *ᵣ-assoc+comm⇒*ₗ-assoc
"Warning: *ᵣ-assoc+comm⇒*ₗ-assoc was deprecated in v2.3.
Please use *ᵣ-assoc∧comm⇒*ₗ-assoc instead."
#-}
*ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc = *ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc
{-# WARNING_ON_USAGE *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc
"Warning: *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc was deprecated in v2.3.
Please use *ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc instead."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4