blob: 929602e93a92d3a29f13fbba1bd395d9d2a9b8a4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
{-# OPTIONS --without-K --safe #-}
open import Algebra using (CommutativeSemiring; CommutativeMonoid)
open import Level using (Level)
module Functor.Forgetful.Instance.Semimodule {c ℓ m ℓm : Level} (R : CommutativeSemiring c ℓ) where
import Algebra.Module.Construct.DirectProduct as DirectProduct
open import Algebra.Module using (Semimodule)
open import Categories.Category using (Category)
open import Categories.Functor using (Functor)
open import Categories.Functor.Cartesian using (IsCartesianF; CartesianF)
open import Category.Cartesian.Instance.CMonoids using (CMonoids-CC)
open import Category.Cartesian.Instance.Semimodules {c} {ℓ} {m} {ℓm} R using (Semimodules-CC; π₁; π₂)
open import Category.Instance.CMonoids using (CMonoids; CMonoidHomomorphism; mk-⇒)
open import Category.Instance.Semimodules {c} {ℓ} {m} {ℓm} R using (Semimodules; SemimoduleHomomorphism)
open import Data.Product using (_,_)
open import Data.Unit.Polymorphic using (tt)
open import Function using (id)
open Semimodule
map : {M N : Semimodule R m ℓm}
→ SemimoduleHomomorphism M N
→ CMonoidHomomorphism m ℓm (+ᴹ-commutativeMonoid M) (+ᴹ-commutativeMonoid N)
map f = mk-⇒ record
{ ⟦_⟧ = ⟦_⟧
; isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism
}
where
open SemimoduleHomomorphism f
+-CMonoid : Functor Semimodules (CMonoids m ℓm)
+-CMonoid = record
{ F₀ = +ᴹ-commutativeMonoid
; F₁ = map
; identity = λ {A} x → ≈ᴹ-refl A {x}
; homomorphism = λ {_ _ C} _ → ≈ᴹ-refl C
; F-resp-≈ = id
}
module +-CMonoid = Functor +-CMonoid
module _ (A B : Semimodule R m ℓm) where
open CMonoidHomomorphism using (⟦_⟧; ⟦⟧-cong; ε-homo; homo)
open Category (CMonoids m ℓm) using (_∘_; _≈_)
private
module A = Semimodule A
module B = Semimodule B
module _
{C : CommutativeMonoid m ℓm}
{f : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid A)}
{g : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid B)} where
<> : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid (DirectProduct.semimodule A B))
<> = mk-⇒ record
{ ⟦_⟧ = λ x → ⟦ f ⟧ x , ⟦ g ⟧ x
; isMonoidHomomorphism = record
{ isMagmaHomomorphism = record
{ isRelHomomorphism = record
{ cong = λ x → ⟦⟧-cong f x , ⟦⟧-cong g x
}
; homo = λ x y → homo f x y , homo g x y
}
; ε-homo = ε-homo f , ε-homo g
}
}
project₁ : map (π₁ A B) ∘ <> ≈ f
project₁ _ = ≈ᴹ-refl A
project₂ : map (π₂ A B) ∘ <> ≈ g
project₂ _ = ≈ᴹ-refl B
unique
: {h : CMonoidHomomorphism m ℓm C (+ᴹ-commutativeMonoid (DirectProduct.semimodule A B))}
→ map (π₁ A B) ∘ h ≈ f
→ map (π₂ A B) ∘ h ≈ g
→ <> ≈ h
unique eq₁ eq₂ x = ≈ᴹ-sym A (eq₁ x) , ≈ᴹ-sym B (eq₂ x)
+-CMonoid-IsCF : IsCartesianF Semimodules-CC CMonoids-CC +-CMonoid
+-CMonoid-IsCF = record
{ F-resp-⊤ = record
{ ! = mk-⇒ record
{ ⟦_⟧ = λ _ → tt
; isMonoidHomomorphism = record
{ isMagmaHomomorphism = record
{ isRelHomomorphism = record
{ cong = λ _ → tt
}
; homo = λ _ _ → tt
}
; ε-homo = tt
}
}
; !-unique = λ _ _ → tt
}
; F-resp-× = λ {A B} → record
{ ⟨_,_⟩ = λ {C} f g → <> A B {C} {f} {g}
; project₁ = λ {C f g} → project₁ A B {C} {f} {g}
; project₂ = λ {C f g} → project₂ A B {C} {f} {g}
; unique = λ {C h f g} → unique A B {C} {f} {g} {h}
}
}
+-CMonoid-CF : CartesianF Semimodules-CC CMonoids-CC
+-CMonoid-CF = record
{ F = +-CMonoid
; isCartesian = +-CMonoid-IsCF
}
|
