From 56c520b69f7211c4bb63827bcbc85081982dd66d Mon Sep 17 00:00:00 2001 From: Laine Taffin Altman Date: Thu, 6 Jun 2024 15:29:44 -0700 Subject: [PATCH] Collapse extrusions Reversible folds into plain, double picks up outer commutes of the underlying heartline. --- src/Algebra/Fumula/Extrusion/Bundles.agda | 38 ------ src/Algebra/Fumula/Extrusion/Construct.agda | 123 ++---------------- src/Algebra/Fumula/Extrusion/Convert.agda | 66 +++++++--- src/Algebra/Fumula/Extrusion/Definitions.agda | 6 +- src/Algebra/Fumula/Extrusion/Structures.agda | 37 ++---- 5 files changed, 76 insertions(+), 194 deletions(-) diff --git a/src/Algebra/Fumula/Extrusion/Bundles.agda b/src/Algebra/Fumula/Extrusion/Bundles.agda index 366b248..af9cdb5 100644 --- a/src/Algebra/Fumula/Extrusion/Bundles.agda +++ b/src/Algebra/Fumula/Extrusion/Bundles.agda @@ -94,24 +94,6 @@ module _ (F : ReversibleAlmostFumula f ℓf) where open DoubleAlmostFumulaExtrusion doubleAlmostFumulaExtrusion public using (❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion; setoid) - record ReversibleAlmostFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where - infix 7 ❲_❳⤙_⤚_ - infix 7 _⤙_⤚❲_❳ - infix 4 _≈_ - field - Carrier : Set x - _≈_ : Rel Carrier ℓx - ❲_❳⤙_⤚_ : Op₃ₗ F.Carrier Carrier - _⤙_⤚❲_❳ : Op₃ᵣ F.Carrier Carrier - isReversibleAlmostFumulaExtrusion : IsReversibleAlmostFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ - open IsReversibleAlmostFumulaExtrusion isReversibleAlmostFumulaExtrusion public - - almostFumulaExtrusion : AlmostFumulaExtrusion x ℓx - almostFumulaExtrusion = record { isAlmostFumulaExtrusion = isAlmostFumulaExtrusion } - open AlmostFumulaExtrusion almostFumulaExtrusion public - using (❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion; - doubleAlmostFumulaExtrusion) - module _ (F : Fumula f ℓf) where private module F = Fumula F @@ -205,23 +187,3 @@ module _ (F : ReversibleFumula f ℓf) where almostFumulaExtrusion : AlmostFumulaExtrusion F.reversibleAlmostFumula x ℓx almostFumulaExtrusion = record { isAlmostFumulaExtrusion = isAlmostFumulaExtrusion } - - record ReversibleFumulaExtrusion (x ℓx : Level) : Set (f ⊔ suc x ⊔ ℓf ⊔ suc ℓx) where - infix 7 ❲_❳⤙_⤚_ - infix 7 _⤙_⤚❲_❳ - infix 4 _≈_ - field - Carrier : Set x - _≈_ : Rel Carrier ℓx - ❲_❳⤙_⤚_ : Op₃ₗ F.Carrier Carrier - _⤙_⤚❲_❳ : Op₃ᵣ F.Carrier Carrier - ◆ : Carrier - isReversibleFumulaExtrusion : IsReversibleFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ - open IsReversibleFumulaExtrusion isReversibleFumulaExtrusion public - - fumulaExtrusion : FumulaExtrusion x ℓx - fumulaExtrusion = record { isFumulaExtrusion = isFumulaExtrusion } - open FumulaExtrusion fumulaExtrusion public - using (❲❳⤙⤚-leftFumulaExtrusion; ⤙⤚❲❳-rightFumulaExtrusion; - ❲❳⤙⤚-leftAlmostFumulaExtrusion; ⤙⤚❲❳-rightAlmostFumulaExtrusion; - doubleFumulaExtrusion; doubleAlmostFumulaExtrusion; almostFumulaExtrusion) diff --git a/src/Algebra/Fumula/Extrusion/Construct.agda b/src/Algebra/Fumula/Extrusion/Construct.agda index 13b2d50..489adaa 100644 --- a/src/Algebra/Fumula/Extrusion/Construct.agda +++ b/src/Algebra/Fumula/Extrusion/Construct.agda @@ -55,11 +55,6 @@ module Terminal {x xℓ} where open AlmostFumulaExtrusion almostFumulaExtrusion public using (isAlmostFumulaExtrusion) - reversibleAlmostFumulaExtrusion : ReversibleAlmostFumulaExtrusion F x xℓ - reversibleAlmostFumulaExtrusion = record { 𝕆ne } - open ReversibleAlmostFumulaExtrusion reversibleAlmostFumulaExtrusion public - using (isReversibleAlmostFumulaExtrusion) - module _ {f fℓ} (F : Fumula f fℓ) where leftFumulaExtrusion : LeftFumulaExtrusion F x xℓ @@ -86,11 +81,6 @@ module Terminal {x xℓ} where open FumulaExtrusion fumulaExtrusion public using (isFumulaExtrusion) - reversibleFumulaExtrusion : ReversibleFumulaExtrusion F x xℓ - reversibleFumulaExtrusion = record { 𝕆ne } - open ReversibleFumulaExtrusion reversibleFumulaExtrusion public - using (isReversibleFumulaExtrusion) - module Initial {x xℓ} where module ℤero where @@ -202,28 +192,15 @@ module Initial {x xℓ} where { isDoubleAlmostFumulaExtrusion = let F′ = ReversibleAlmostFumula.almostFumula F in isDoubleAlmostFumulaExtrusion F′ F′ + ; outer-commute = λ () } } open AlmostFumulaExtrusion almostFumulaExtrusion public using (isAlmostFumulaExtrusion) - reversibleAlmostFumulaExtrusion : ReversibleAlmostFumulaExtrusion F x xℓ - reversibleAlmostFumulaExtrusion = record - { Carrier = Carrier - ; _≈_ = _≈_ - ; ❲_❳⤙_⤚_ = ❲_❳⤙_⤚_ - ; _⤙_⤚❲_❳ = _⤙_⤚❲_❳ - ; isReversibleAlmostFumulaExtrusion = record { - isAlmostFumulaExtrusion = isAlmostFumulaExtrusion - ; outer-commute = λ () - } - } - open ReversibleAlmostFumulaExtrusion reversibleAlmostFumulaExtrusion public - using (isReversibleAlmostFumulaExtrusion) - open Terminal {x} {xℓ} public hiding (module 𝕆ne; isEquivalence; leftAlmostFumulaExtrusion; rightAlmostFumulaExtrusion; - doubleAlmostFumulaExtrusion; almostFumulaExtrusion; reversibleAlmostFumulaExtrusion) + doubleAlmostFumulaExtrusion; almostFumulaExtrusion) module DirectProduct {x₁ xℓ₁ x₂ xℓ₂} where @@ -308,30 +285,12 @@ module DirectProduct {x₁ xℓ₁ x₂ xℓ₂} where { isDoubleAlmostFumulaExtrusion = let F′ = ReversibleAlmostFumula.almostFumula F in isDoubleAlmostFumulaExtrusion F′ F′ X₁.doubleAlmostFumulaExtrusion X₂.doubleAlmostFumulaExtrusion + ; outer-commute = λ (y₁ , y₂) x (z₁ , z₂) → X₁.outer-commute y₁ x z₁ , X₂.outer-commute y₂ x z₂ } } open AlmostFumulaExtrusion almostFumulaExtrusion public using (isAlmostFumulaExtrusion) - module _ {f fℓ} (F : ReversibleAlmostFumula f fℓ) (X₁ : ReversibleAlmostFumulaExtrusion F x₁ xℓ₁) (X₂ : ReversibleAlmostFumulaExtrusion F x₂ xℓ₂) where - private - module X₁ = ReversibleAlmostFumulaExtrusion X₁ - module X₂ = ReversibleAlmostFumulaExtrusion X₂ - - reversibleAlmostFumulaExtrusion : ReversibleAlmostFumulaExtrusion F (x₁ ⊔ x₂) (xℓ₁ ⊔ xℓ₂) - reversibleAlmostFumulaExtrusion = record - { Carrier = X₁.Carrier × X₂.Carrier - ; _≈_ = Pointwise X₁._≈_ X₂._≈_ - ; ❲_❳⤙_⤚_ = λ s (z₁ , z₂) (x₁ , x₂) → (X₁.❲ s ❳⤙ z₁ ⤚ x₁) , (X₂.❲ s ❳⤙ z₂ ⤚ x₂) - ; _⤙_⤚❲_❳ = λ (x₁ , x₂) (z₁ , z₂) s → (x₁ X₁.⤙ z₁ ⤚❲ s ❳) , (x₂ X₂.⤙ z₂ ⤚❲ s ❳) - ; isReversibleAlmostFumulaExtrusion = record - { isAlmostFumulaExtrusion = isAlmostFumulaExtrusion F X₁.almostFumulaExtrusion X₂.almostFumulaExtrusion - ; outer-commute = λ (y₁ , y₂) x (z₁ , z₂) → X₁.outer-commute y₁ x z₁ , X₂.outer-commute y₂ x z₂ - } - } - open ReversibleAlmostFumulaExtrusion reversibleAlmostFumulaExtrusion public - using (isReversibleAlmostFumulaExtrusion) - module _ {f fℓ} (F : Fumula f fℓ) (X₁ : LeftFumulaExtrusion F x₁ xℓ₁) (X₂ : LeftFumulaExtrusion F x₂ xℓ₂) where private module X₁ = LeftFumulaExtrusion X₁ @@ -413,6 +372,9 @@ module DirectProduct {x₁ xℓ₁ x₂ xℓ₂} where ; ⤙⤚❲❳-◆-collapse-middleˡ = λ x (z₁ , z₂) → X₁.⤙⤚❲❳-◆-collapse-middleˡ x z₁ , X₂.⤙⤚❲❳-◆-collapse-middleˡ x z₂ ; ⤙⤚❲❳-◆ᶠ-collapse-middleʳ = λ (x₁ , x₂) (z₁ , z₂) → X₁.⤙⤚❲❳-◆ᶠ-collapse-middleʳ x₁ z₁ , X₂.⤙⤚❲❳-◆ᶠ-collapse-middleʳ x₂ z₂ ; ⤙⤚❲❳-◆ᶠ-◆-outer-associate = λ (w₁ , w₂) x y (z₁ , z₂) → X₁.⤙⤚❲❳-◆ᶠ-◆-outer-associate w₁ x y z₁ , X₂.⤙⤚❲❳-◆ᶠ-◆-outer-associate w₂ x y z₂ + ; ■ᶠ-outer-commute = λ (x₁ , x₂) (z₁ , z₂) → X₁.■ᶠ-outer-commute x₁ z₁ , X₂.■ᶠ-outer-commute x₂ z₂ + ; ◆ᶠ-outer-commute = λ (x₁ , x₂) (z₁ , z₂) → X₁.◆ᶠ-outer-commute x₁ z₁ , X₂.◆ᶠ-outer-commute x₂ z₂ + ; ●ᶠ-outer-commute = λ (x₁ , x₂) (z₁ , z₂) → X₁.●ᶠ-outer-commute x₁ z₁ , X₂.●ᶠ-outer-commute x₂ z₂ ; ◆-outer-associate = λ w (x₁ , x₂) y (z₁ , z₂) → X₁.◆-outer-associate w x₁ y z₁ , X₂.◆-outer-associate w x₂ y z₂ } } @@ -435,35 +397,12 @@ module DirectProduct {x₁ xℓ₁ x₂ xℓ₂} where { isDoubleFumulaExtrusion = let F′ = ReversibleFumula.fumula F in isDoubleFumulaExtrusion F′ F′ X₁.doubleFumulaExtrusion X₂.doubleFumulaExtrusion - ; ■ᶠ-outer-commute = λ (x₁ , x₂) (z₁ , z₂) → X₁.■ᶠ-outer-commute x₁ z₁ , X₂.■ᶠ-outer-commute x₂ z₂ - ; ◆ᶠ-outer-commute = λ (x₁ , x₂) (z₁ , z₂) → X₁.◆ᶠ-outer-commute x₁ z₁ , X₂.◆ᶠ-outer-commute x₂ z₂ - ; ●ᶠ-outer-commute = λ (x₁ , x₂) (z₁ , z₂) → X₁.●ᶠ-outer-commute x₁ z₁ , X₂.●ᶠ-outer-commute x₂ z₂ - ; ◆-outer-commute = λ x (z₁ , z₂) → X₁.◆-outer-commute x z₁ , X₂.◆-outer-commute x z₂ + ; outer-commute = λ (y₁ , y₂) x (z₁ , z₂) → X₁.outer-commute y₁ x z₁ , X₂.outer-commute y₂ x z₂ } } open FumulaExtrusion fumulaExtrusion public using (isFumulaExtrusion) - module _ {f fℓ} (F : ReversibleFumula f fℓ) (X₁ : ReversibleFumulaExtrusion F x₁ xℓ₁) (X₂ : ReversibleFumulaExtrusion F x₂ xℓ₂) where - private - module X₁ = ReversibleFumulaExtrusion X₁ - module X₂ = ReversibleFumulaExtrusion X₂ - - reversibleFumulaExtrusion : ReversibleFumulaExtrusion F (x₁ ⊔ x₂) (xℓ₁ ⊔ xℓ₂) - reversibleFumulaExtrusion = record - { Carrier = X₁.Carrier × X₂.Carrier - ; _≈_ = Pointwise X₁._≈_ X₂._≈_ - ; ❲_❳⤙_⤚_ = λ s (z₁ , z₂) (x₁ , x₂) → (X₁.❲ s ❳⤙ z₁ ⤚ x₁) , (X₂.❲ s ❳⤙ z₂ ⤚ x₂) - ; _⤙_⤚❲_❳ = λ (x₁ , x₂) (z₁ , z₂) s → (x₁ X₁.⤙ z₁ ⤚❲ s ❳) , (x₂ X₂.⤙ z₂ ⤚❲ s ❳) - ; ◆ = X₁.◆ , X₂.◆ - ; isReversibleFumulaExtrusion = record - { isFumulaExtrusion = isFumulaExtrusion F X₁.fumulaExtrusion X₂.fumulaExtrusion - ; outer-commute = λ (y₁ , y₂) x (z₁ , z₂) → X₁.outer-commute y₁ x z₁ , X₂.outer-commute y₂ x z₂ - } - } - open ReversibleFumulaExtrusion reversibleFumulaExtrusion public - using (isReversibleFumulaExtrusion) - module TensorUnit {f fℓ} where module _ (F : AlmostFumula f fℓ) where @@ -492,26 +431,6 @@ module TensorUnit {f fℓ} where ⤙⤚❲❳-rightAlmostFumulaExtrusion to rightAlmostFumulaExtrusion; ⤙⤚❲❳-isRightAlmostFumulaExtrusion to isRightAlmostFumulaExtrusion) - module _ (F : ReversibleAlmostFumula f fℓ) where - private - module F = ReversibleAlmostFumula F - - reversibleAlmostFumulaExtrusion : ReversibleAlmostFumulaExtrusion F f fℓ - reversibleAlmostFumulaExtrusion = record - { Carrier = F.Carrier - ; _≈_ = F._≈_ - ; ❲_❳⤙_⤚_ = F._⤙_⤚_ - ; _⤙_⤚❲_❳ = F._⤙_⤚_ - ; isReversibleAlmostFumulaExtrusion = record - { isAlmostFumulaExtrusion = record - { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion F.almostFumula - } - ; outer-commute = F.outer-commute - } - } - open ReversibleAlmostFumulaExtrusion reversibleAlmostFumulaExtrusion public - using (almostFumulaExtrusion; isAlmostFumulaExtrusion; isReversibleAlmostFumulaExtrusion) - module _ (F : Fumula f fℓ) where private module F = Fumula F @@ -539,6 +458,9 @@ module TensorUnit {f fℓ} where ; ⤙⤚❲❳-◆-collapse-middleˡ = F.◆-collapse-middleˡ ; ⤙⤚❲❳-◆ᶠ-collapse-middleʳ = F.◆-collapse-middleʳ ; ⤙⤚❲❳-◆ᶠ-◆-outer-associate = F.◆-outer-associate + ; ■ᶠ-outer-commute = λ x z → F.■-outer-commute x z + ; ◆ᶠ-outer-commute = λ x z → F.◆-outer-commute x z + ; ●ᶠ-outer-commute = λ x z → F.●-outer-commute x z ; ◆-outer-associate = F.◆-outer-associate } } @@ -548,28 +470,3 @@ module TensorUnit {f fℓ} where ❲❳⤙⤚-isLeftFumulaExtrusion to isLeftFumulaExtrusion; ⤙⤚❲❳-rightFumulaExtrusion to rightFumulaExtrusion; ⤙⤚❲❳-isRightFumulaExtrusion to isRightFumulaExtrusion) - - module _ (F : ReversibleFumula f fℓ) where - private - module F = ReversibleFumula F - - reversibleFumulaExtrusion : ReversibleFumulaExtrusion F f fℓ - reversibleFumulaExtrusion = record - { Carrier = F.Carrier - ; _≈_ = F._≈_ - ; ❲_❳⤙_⤚_ = F._⤙_⤚_ - ; _⤙_⤚❲_❳ = F._⤙_⤚_ - ; ◆ = F.◆ - ; isReversibleFumulaExtrusion = record - { isFumulaExtrusion = record - { isDoubleFumulaExtrusion = isDoubleFumulaExtrusion F.fumula - ; ■ᶠ-outer-commute = F.■-outer-commute - ; ◆ᶠ-outer-commute = F.◆-outer-commute - ; ●ᶠ-outer-commute = F.●-outer-commute - ; ◆-outer-commute = F.◆-outer-commute - } - ; outer-commute = F.outer-commute - } - } - open ReversibleFumulaExtrusion reversibleFumulaExtrusion public - using (fumulaExtrusion; isFumulaExtrusion; isReversibleFumulaExtrusion) diff --git a/src/Algebra/Fumula/Extrusion/Convert.agda b/src/Algebra/Fumula/Extrusion/Convert.agda index f69e969..c550b2b 100644 --- a/src/Algebra/Fumula/Extrusion/Convert.agda +++ b/src/Algebra/Fumula/Extrusion/Convert.agda @@ -12,11 +12,11 @@ open import Relation.Binary.Structures using (IsEquivalence) import Relation.Binary.Reasoning.Setoid as SetoidReasoning open import Algebra.Core open import Algebra.Bundles +import Algebra.Properties.Group as GroupProperties import Algebra.Properties.Ring as RingProperties open import Algebra.Module.Core open import Algebra.Module.Structures open import Algebra.Module.Bundles -import Algebra.Module.Properties as ModuleProperties open import Algebra.Module.Morphism.Structures import Algebra.Module.Morphism.ModuleHomomorphism as ModuleHomomorphismProperties open import Algebra.Fumula.Core using (Op₃) @@ -258,6 +258,24 @@ module FromModule where ; ⤙⤚❲❳-◆-collapse-middleˡ = ⤙⤚❲❳-◆-collapse-middleˡ ; ⤙⤚❲❳-◆ᶠ-collapse-middleʳ = ⤙⤚❲❳-◆ᶠ-collapse-middleʳ ; ⤙⤚❲❳-◆ᶠ-◆-outer-associate = ⤙⤚❲❳-◆ᶠ-◆-outer-associate + ; ■ᶠ-outer-commute = λ x z → +ᴹ-congʳ (begin + x *ᵣ (Rᵣ.- Rᵣ.1#) ≈⟨ -ᴹ⇒-‿distribʳ-*ᵣ x Rᵣ.1# ⟨ + - (x *ᵣ Rᵣ.1#) ≈⟨ -ᴹ‿cong (*ᵣ-identityʳ x) ⟩ + - x ≈⟨ -ᴹ‿cong (*ₗ-identityˡ x) ⟨ + - (Rₗ.1# *ₗ x) ≈⟨ -ᴹ⇒-‿distribˡ-*ₗ Rₗ.1# x ⟩ + (Rₗ.- Rₗ.1#) *ₗ x ∎) + ; ◆ᶠ-outer-commute = λ x z → +ᴹ-congʳ (begin + x *ᵣ (Rᵣ.- Rᵣ.1# Rᵣ.* Rᵣ.- Rᵣ.1# Rᵣ.+ Rᵣ.- Rᵣ.1#) ≈⟨ *ᵣ-congˡ Rᵣ.0≈-1*-1+-1 ⟨ + x *ᵣ Rᵣ.0# ≈⟨ *ᵣ-zeroʳ x ⟩ + 0# ≈⟨ *ₗ-zeroˡ x ⟨ + Rₗ.0# *ₗ x ≈⟨ *ₗ-congʳ Rₗ.0≈-1*-1+-1 ⟩ + (Rₗ.- Rₗ.1# Rₗ.* Rₗ.- Rₗ.1# Rₗ.+ Rₗ.- Rₗ.1#) *ₗ x ∎) + ; ●ᶠ-outer-commute = λ x z → +ᴹ-congʳ (begin + x *ᵣ (Rᵣ.- Rᵣ.1# Rᵣ.* Rᵣ.- Rᵣ.1# Rᵣ.+ (Rᵣ.- Rᵣ.1# Rᵣ.* Rᵣ.- Rᵣ.1# Rᵣ.+ Rᵣ.- Rᵣ.1#)) ≈⟨ *ᵣ-congˡ Rᵣ.1≈-1*-1+[-1*-1+-1] ⟨ + x *ᵣ Rᵣ.1# ≈⟨ *ᵣ-identityʳ x ⟩ + x ≈⟨ *ₗ-identityˡ x ⟨ + Rₗ.1# *ₗ x ≈⟨ *ₗ-congʳ Rₗ.1≈-1*-1+[-1*-1+-1] ⟩ + (Rₗ.- Rₗ.1# Rₗ.* Rₗ.- Rₗ.1# Rₗ.+ (Rₗ.- Rₗ.1# Rₗ.* Rₗ.- Rₗ.1# Rₗ.+ Rₗ.- Rₗ.1#)) *ₗ x ∎) ; ◆-outer-associate = λ w x y z → +ᴹ-congʳ (begin ((w *ₗ x) + 0#) *ᵣ y ≈⟨ *ᵣ-congʳ (+ᴹ-identityʳ (w *ₗ x)) ⟩ (w *ₗ x) *ᵣ y ≈⟨ *ₗ-*ᵣ-assoc w x y ⟩ @@ -269,6 +287,29 @@ module FromModule where open IsLeftFumulaExtrusion (isLeftFumulaExtrusion Rₗ _≈_ _+_ 0# -_ _*ₗ_ isLeftModule) hiding (isEquivalence) open IsRightFumulaExtrusion (isRightFumulaExtrusion Rᵣ _≈_ _+_ 0# -_ _*ᵣ_ isRightModule) hiding (isEquivalence) open SetoidReasoning record { isEquivalence = ≈ᴹ-isEquivalence } + open IsEquivalence ≈ᴹ-isEquivalence using (sym) + + -ᴹ⇒-‿distribˡ-*ₗ : ∀ x y → (- (x *ₗ y)) ≈ ((Rₗ.- x) *ₗ y) + -ᴹ⇒-‿distribˡ-*ₗ x y = sym (begin + (Rₗ.- x) *ₗ y ≈⟨ +ᴹ-identityʳ ((Rₗ.- x) *ₗ y) ⟨ + ((Rₗ.- x) *ₗ y) + 0# ≈⟨ +ᴹ-congˡ (-ᴹ‿inverseʳ (x *ₗ y)) ⟨ + ((Rₗ.- x) *ₗ y) + ((x *ₗ y) + (- (x *ₗ y))) ≈⟨ +ᴹ-assoc ((Rₗ.- x) *ₗ y) (x *ₗ y) (- (x *ₗ y)) ⟨ + (((Rₗ.- x) *ₗ y) + (x *ₗ y)) + (- (x *ₗ y)) ≈⟨ +ᴹ-congʳ (*ₗ-distribʳ y (Rₗ.- x) x) ⟨ + ((((Rₗ.- x) Rₗ.+ x) *ₗ y) + (- (x *ₗ y))) ≈⟨ +ᴹ-congʳ (*ₗ-congʳ (Rₗ.-‿inverseˡ x)) ⟩ + ((Rₗ.0# *ₗ y) + (- (x *ₗ y))) ≈⟨ +ᴹ-congʳ (*ₗ-zeroˡ y) ⟩ + (0# + (- (x *ₗ y))) ≈⟨ +ᴹ-identityˡ (- (x *ₗ y)) ⟩ + - (x *ₗ y) ∎) + + -ᴹ⇒-‿distribʳ-*ᵣ : ∀ x y → (- (x *ᵣ y)) ≈ (x *ᵣ (Rᵣ.- y)) + -ᴹ⇒-‿distribʳ-*ᵣ x y = sym (begin + x *ᵣ (Rᵣ.- y) ≈⟨ +ᴹ-identityˡ (x *ᵣ (Rᵣ.- y)) ⟨ + 0# + (x *ᵣ (Rᵣ.- y)) ≈⟨ +ᴹ-congʳ (-ᴹ‿inverseˡ (x *ᵣ y)) ⟨ + ((- (x *ᵣ y)) + (x *ᵣ y)) + (x *ᵣ (Rᵣ.- y)) ≈⟨ +ᴹ-assoc (- (x *ᵣ y)) (x *ᵣ y) (x *ᵣ (Rᵣ.- y)) ⟩ + (- (x *ᵣ y)) + ((x *ᵣ y) + (x *ᵣ (Rᵣ.- y))) ≈⟨ +ᴹ-congˡ (*ᵣ-distribˡ x y (Rᵣ.- y)) ⟨ + (- (x *ᵣ y)) + (x *ᵣ (y Rᵣ.+ Rᵣ.- y)) ≈⟨ +ᴹ-congˡ (*ᵣ-congˡ (Rᵣ.-‿inverseʳ y)) ⟩ + (- (x *ᵣ y)) + (x *ᵣ Rᵣ.0#) ≈⟨ +ᴹ-congˡ (*ᵣ-zeroʳ x) ⟩ + (- (x *ᵣ y)) + 0# ≈⟨ +ᴹ-identityʳ (- (x *ᵣ y)) ⟩ + - (x *ᵣ y) ∎) module _ {rₗ rᵣ m rℓₗ rℓᵣ mℓ} (Rₗ : Ring rₗ rℓₗ) (Rᵣ : Ring rᵣ rℓᵣ) where private @@ -304,15 +345,9 @@ module FromModule where ◆ : Carrier ◆ = 0# - isReversibleFumulaExtrusion : IsModule R _≈_ _+_ 0# -_ _*ₗ_ _*ᵣ_ → IsReversibleFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ - isReversibleFumulaExtrusion M = record - { isFumulaExtrusion = record - { isDoubleFumulaExtrusion = iDFE - ; ■ᶠ-outer-commute = λ x _ → +ᴹ-congʳ (sym (*ₗ-*ᵣ-coincident F.■ x)) - ; ◆ᶠ-outer-commute = λ x _ → +ᴹ-congʳ (sym (*ₗ-*ᵣ-coincident F.◆ x)) - ; ●ᶠ-outer-commute = λ x _ → +ᴹ-congʳ (sym (*ₗ-*ᵣ-coincident F.● x)) - ; ◆-outer-commute = λ x _ → +ᴹ-congʳ (*ₗ-*ᵣ-coincident x 0#) - } + isFumulaExtrusion : IsModule R _≈_ _+_ 0# -_ _*ₗ_ _*ᵣ_ → IsFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ + isFumulaExtrusion M = record + { isDoubleFumulaExtrusion = iDFE ; outer-commute = λ y x _ → +ᴹ-congʳ (*ₗ-*ᵣ-coincident x y) } where @@ -320,7 +355,6 @@ module FromModule where iDFE : IsDoubleFumulaExtrusion F.fumula F.fumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ iDFE = isDoubleFumulaExtrusion R.ring R.ring _≈_ _+_ 0# -_ _*ₗ_ _*ᵣ_ isBimodule open IsDoubleFumulaExtrusion iDFE - open IsEquivalence isEquivalence using (sym) module FromFumulaExtrusion where @@ -640,13 +674,13 @@ module FromFumulaExtrusion where _*ᵣ_ : Opᵣ R.Carrier Carrier x *ᵣ s = x ⤙ ◆ ⤚❲ s ❳ - isModule : IsReversibleFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ → IsModule R _≈_ _+_ 0# -_ _*ₗ_ _*ᵣ_ + isModule : IsFumulaExtrusion F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ → IsModule R _≈_ _+_ 0# -_ _*ₗ_ _*ᵣ_ isModule X = record { isBimodule = iB ; *ₗ-*ᵣ-coincident = λ x s → outer-commute s x ◆ } where - open IsReversibleFumulaExtrusion X + open IsFumulaExtrusion X iB : IsBimodule R.ring R.ring _≈_ _+_ 0# -_ _*ₗ_ _*ᵣ_ iB = isBimodule F.fumula F.fumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ isDoubleFumulaExtrusion open IsBimodule iB @@ -656,6 +690,6 @@ module FromFumulaExtrusion where R : CommutativeRing f fℓ R = FromFumula.commutativeRing F - ‵module : ReversibleFumulaExtrusion F x xℓ → Module R x xℓ - ‵module X = record { isModule = isModule F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ isReversibleFumulaExtrusion } - where open ReversibleFumulaExtrusion X + ‵module : FumulaExtrusion F x xℓ → Module R x xℓ + ‵module X = record { isModule = isModule F _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ isFumulaExtrusion } + where open FumulaExtrusion X diff --git a/src/Algebra/Fumula/Extrusion/Definitions.agda b/src/Algebra/Fumula/Extrusion/Definitions.agda index d0aa8a1..c7c054a 100644 --- a/src/Algebra/Fumula/Extrusion/Definitions.agda +++ b/src/Algebra/Fumula/Extrusion/Definitions.agda @@ -59,6 +59,9 @@ module BiDefs {aₗ aᵣ b ℓb} {Aₗ : Set aₗ} {Aᵣ : Set aᵣ} {B : Set b} MiddleNestedDoubleExchange : Set _ MiddleNestedDoubleExchange = ∀ v w x y z → (❲ v ❳⤙ x ⤙ z ⤚❲ y ❳ ⤚ w) ≈ᵇ (x ⤙ ❲ v ❳⤙ z ⤚ w ⤚❲ y ❳) + OuterCommutativeWithUnderlying : Aₗ → Aᵣ → Set _ + OuterCommutativeWithUnderlying eₗ eᵣ = ∀ x z → (x ⤙ z ⤚❲ eᵣ ❳) ≈ᵇ (❲ eₗ ❳⤙ z ⤚ x) + OuterAssociativeWith : B → Set _ OuterAssociativeWith e = ∀ w x y z → ((❲ w ❳⤙ e ⤚ x) ⤙ z ⤚❲ y ❳) ≈ᵇ (❲ w ❳⤙ z ⤚ (x ⤙ e ⤚❲ y ❳)) @@ -69,9 +72,10 @@ module SimultaneousBiDefs {a b ℓb} {A : Set a} {B : Set b} (❲_❳⤙_⤚_ : private module L = LeftDefs ❲_❳⤙_⤚_ _≈ᵇ_ module R = RightDefs _⤙_⤚❲_❳ _≈ᵇ_ + module B = BiDefs ❲_❳⤙_⤚_ _⤙_⤚❲_❳ _≈ᵇ_ OuterCommutativeWithUnderlying : A → Set _ - OuterCommutativeWithUnderlying e = ∀ x z → (x ⤙ z ⤚❲ e ❳) ≈ᵇ (❲ e ❳⤙ z ⤚ x) + OuterCommutativeWithUnderlying e = B.OuterCommutativeWithUnderlying e e OuterCommutativeWith : B → Set _ OuterCommutativeWith e = ∀ x z → (❲ x ❳⤙ z ⤚ e) ≈ᵇ (e ⤙ z ⤚❲ x ❳) diff --git a/src/Algebra/Fumula/Extrusion/Structures.agda b/src/Algebra/Fumula/Extrusion/Structures.agda index 5e4d273..081f492 100644 --- a/src/Algebra/Fumula/Extrusion/Structures.agda +++ b/src/Algebra/Fumula/Extrusion/Structures.agda @@ -94,19 +94,13 @@ module _ (F : ReversibleAlmostFumula f ℓf) (_≈_ : Rel {x} X ℓx) module F = ReversibleAlmostFumula F record IsAlmostFumulaExtrusion : Set (f ⊔ x ⊔ ℓf ⊔ ℓx) where - field - isDoubleAlmostFumulaExtrusion : IsDoubleAlmostFumulaExtrusion F.almostFumula F.almostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ - - open IsDoubleAlmostFumulaExtrusion isDoubleAlmostFumulaExtrusion public - - record IsReversibleAlmostFumulaExtrusion : Set (f ⊔ x ⊔ ℓf ⊔ ℓx) where open SimultaneousBiDefs ❲_❳⤙_⤚_ _⤙_⤚❲_❳ _≈_ field - isAlmostFumulaExtrusion : IsAlmostFumulaExtrusion + isDoubleAlmostFumulaExtrusion : IsDoubleAlmostFumulaExtrusion F.almostFumula F.almostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ outer-commute : OuterCommutative - open IsAlmostFumulaExtrusion isAlmostFumulaExtrusion public + open IsDoubleAlmostFumulaExtrusion isDoubleAlmostFumulaExtrusion public module _ (F : Fumula f ℓf) (_≈_ : Rel {x} X ℓx) (❲_❳⤙_⤚_ : Op₃ₗ (Fumula.Carrier F) X) (◆ : X) where @@ -178,6 +172,9 @@ module _ (Fₗ : Fumula fₗ ℓfₗ) (Fᵣ : Fumula fᵣ ℓfᵣ) (_≈_ : Rel ⤙⤚❲❳-◆-collapse-middleˡ : ∀ x z → (◆ ⤙ z ⤚❲ x ❳) ≈ z ⤙⤚❲❳-◆ᶠ-collapse-middleʳ : ∀ x z → (x ⤙ z ⤚❲ Fᵣ.◆ ❳) ≈ z ⤙⤚❲❳-◆ᶠ-◆-outer-associate : R.OuterAssociativeWith Fᵣ._⤙_⤚_ Fᵣ.◆ ◆ + ■ᶠ-outer-commute : OuterCommutativeWithUnderlying Fₗ.■ Fᵣ.■ + ◆ᶠ-outer-commute : OuterCommutativeWithUnderlying Fₗ.◆ Fᵣ.◆ + ●ᶠ-outer-commute : OuterCommutativeWithUnderlying Fₗ.● Fᵣ.● ◆-outer-associate : OuterAssociativeWith ◆ open IsDoubleAlmostFumulaExtrusion isDoubleAlmostFumulaExtrusion public @@ -221,33 +218,21 @@ module _ (F : ReversibleFumula f ℓf) (_≈_ : Rel {x} X ℓx) field isDoubleFumulaExtrusion : IsDoubleFumulaExtrusion F.fumula F.fumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ ◆ - ■ᶠ-outer-commute : OuterCommutativeWithUnderlying F.■ - ◆ᶠ-outer-commute : OuterCommutativeWithUnderlying F.◆ - ●ᶠ-outer-commute : OuterCommutativeWithUnderlying F.● - ◆-outer-commute : OuterCommutativeWith ◆ + outer-commute : OuterCommutative open IsDoubleFumulaExtrusion isDoubleFumulaExtrusion public ●ᶠ-inner-commute : InnerCommutativeWith F.● ●ᶠ-inner-commute = ⤙⤚❲❳-●ᶠ-inner-commuteˡ , ❲❳⤙⤚-●ᶠ-inner-commuteʳ + ◆-outer-commute : OuterCommutativeWith ◆ + ◆-outer-commute = outer-commute ◆ + ◆ᶠ-pullout : PulloutWith F._⤙_⤚_ F.◆ ◆ᶠ-pullout = ❲❳⤙⤚-◆ᶠ-pulloutˡ , ⤙⤚❲❳-◆ᶠ-pulloutʳ isAlmostFumulaExtrusion : IsAlmostFumulaExtrusion F.reversibleAlmostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ - isAlmostFumulaExtrusion = record { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion } - - record IsReversibleFumulaExtrusion : Set (f ⊔ x ⊔ ℓf ⊔ ℓx) where - open SimultaneousBiDefs ❲_❳⤙_⤚_ _⤙_⤚❲_❳ _≈_ - - field - isFumulaExtrusion : IsFumulaExtrusion - outer-commute : OuterCommutative - - open IsFumulaExtrusion isFumulaExtrusion public - - isReversibleAlmostFumulaExtrusion : IsReversibleAlmostFumulaExtrusion F.reversibleAlmostFumula _≈_ ❲_❳⤙_⤚_ _⤙_⤚❲_❳ - isReversibleAlmostFumulaExtrusion = record - { isAlmostFumulaExtrusion = isAlmostFumulaExtrusion + isAlmostFumulaExtrusion = record + { isDoubleAlmostFumulaExtrusion = isDoubleAlmostFumulaExtrusion ; outer-commute = outer-commute }