Elienberg Moore Category
Menu MenuElienberg Moore Category
examples/em-category.agda Monad は、もう一つのResolutionを持っており、Kleisli Category のように Comparison Functor を構成することができます。Elienberg Moore Category は Monoids 同じような構造を持っています。これから出てくる homomorphism とかは、そこから来ています。
今度は射は、Aの射をそのまま使います。対象 Obj は Algebra と呼ばれる制約が付きます。
まず、module の引数で道具をそろえます。Monad M(T, η, μ) です。
module em-category { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ }
{ T : Functor A A }
{ η : NTrans A A identityFunctor T }
{ μ : NTrans A A (T ○ T) T }
{ M : Monad A T η μ } where
Obj は record として用意します。
record IsAlgebra {a : Obj A} { phi : Hom A (FObj T a) a } : Set (c₁ ⊔ c₂ ⊔ ℓ) where
field
identity : A [ A [ phi o TMap η a ] ≈ id1 A a ]
eval : A [ A [ phi o TMap μ a ] ≈ A [ phi o FMap T phi ] ]
record EMObj : Set (c₁ ⊔ c₂ ⊔ ℓ) where
field
a : Obj A
phi : Hom A (FObj T a) a
isAlgebra : IsAlgebra {a} {phi}
obj : Obj A
obj = a
φ : Hom A (FObj T a) a
φ = phi
open EMObj
a は Obj そのものですが、Obj には φ : T(a)->a という射が付属していています。
射は、a の射そのものですが、やはり制約があります。
record Eilenberg-Moore-Hom (a : EMObj ) (b : EMObj ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
field
EMap : Hom A (obj a) (obj b)
homomorphism : A [ A [ (φ b) o FMap T EMap ] ≈ A [ EMap o (φ a) ] ]
open Eilenberg-Moore-Hom
EMHom : (a : EMObj ) (b : EMObj ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
EMHom = \a b -> Eilenberg-Moore-Hom a b
制約があるのとElienberg Moore Category の対象からの関数に直す必要があるので、やはり record にする必要があります。
φが満たす可換図を書くと、以下の様になります。
η(a) μ(a) T(f)
a-----------> T(a) T^2(a)--------> T(a) T(a)---------->T(b)
| | | | |
| | | | |
|φ T(φ)| |φ φ| |φ'
| | | | |
v v v v v
_ a T(a)-------->T(a) a------------> b
φ f
単位射は A の単位射そのものですが、制約を満たしているかどうかを確認する必要があります。制約を満たしているという証明を record に登録する必要があるわけです。
Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj )
-> A [ A [ φ o FMap T (id1 A x) ] ≈ A [ (id1 A x) o φ ] ]
Lemma-EM1 {x} {φ} a = let open ≈-Reasoning (A) in
begin
φ o FMap T (id1 A x)
≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
φ o (id1 A (FObj T x))
≈⟨ idR ⟩
φ
≈⟨ sym idL ⟩
(id1 A x) o φ
∎
EM-id : { a : EMObj } -> EMHom a a
EM-id {a} = record { EMap = id1 A (obj a);
homomorphism = Lemma-EM1 {obj a} {phi a} a }
合成も合成自体は同じですが、homorphism を証明しなくてはなりません。
open import Relation.Binary.Core
Lemma-EM2 : (a : EMObj )
(b : EMObj )
(c : EMObj )
(g : EMHom b c)
(f : EMHom a b)
-> A [ A [ φ c o FMap T (A [ (EMap g) o (EMap f) ] ) ]
≈ A [ (A [ (EMap g) o (EMap f) ]) o φ a ] ]
Lemma-EM2 a b c g f = let
open ≈-Reasoning (A) in
begin
φ c o FMap T ((EMap g) o (EMap f))
≈⟨ cdr (distr T) ⟩
φ c o ( FMap T (EMap g) o FMap T (EMap f) )
≈⟨ assoc ⟩
( φ c o FMap T (EMap g)) o FMap T (EMap f)
≈⟨ car (homomorphism (g)) ⟩
( EMap g o φ b) o FMap T (EMap f)
≈⟨ sym assoc ⟩
EMap g o (φ b o FMap T (EMap f) )
≈⟨ cdr (homomorphism (f)) ⟩
EMap g o (EMap f o φ a)
≈⟨ assoc ⟩
( (EMap g) o (EMap f) ) o φ a
∎
_∙_ : {a b c : EMObj } -> EMHom b c -> EMHom a b -> EMHom a c
_∙_ {a} {b} {c} g f = record { EMap = A [ EMap g o EMap f ] ; homomorphism = Lemma-EM2 a b c g f }
合成する射の homomorphism の合成によって証明を得ることができます。
等式はそのままです。
_≗_ : {a : EMObj } {b : EMObj } (f g : EMHom a b ) -> Set ℓ
_≗_ f g = A [ EMap f ≈ EMap g ]
Category の性質は射に関するものだけで、射自体はAと同じで、合成に関して homomoprhism が成立することがわかっているので、Category の性質は、すべて A の性質に帰着することができます。
isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id
isEilenberg-MooreCategory = record { isEquivalence = isEquivalence
; identityL = IsCategory.identityL (Category.isCategory A)
; identityR = IsCategory.identityR (Category.isCategory A)
; o-resp-≈ = IsCategory.o-resp-≈ (Category.isCategory A)
; associative = IsCategory.associative (Category.isCategory A)
}
where
open ≈-Reasoning (A)
isEquivalence : {a : EMObj } {b : EMObj } ->
IsEquivalence {_} {_} {EMHom a b } _≗_
isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types
record { refl = refl-hom
; sym = sym
; trans = trans-hom
}
Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ
Eilenberg-MooreCategory =
record { Obj = EMObj
; Hom = EMHom
; _o_ = _∙_
; _≈_ = _≗_
; Id = EM-id
; isCategory = isEilenberg-MooreCategory
}
Equivalence を一度分解する必要があるのはいつもの通りです。
Monoid Monad に対する Elienberg Moore Category
f: a-> b
T: a -> (m,a)
η: a -> (1,a)
μ: (m,(m',a)) -> (mm',a)
でした。φは、以下のようになります。
φ: (m,a) -> φ(m,a) = ma
制約を証明する必要がありますが、Monad なことはわかっているので、既に証明は終わっています。
η(a) μ(a) T(f)
a----------->(1,a) (m,(m',a))-----> (mm',a) (m,a)----------->(m,f(a))
| | | | |
| | | | |
|φ T(φ)| |φ φ| |φ'
| | | | |
v v v v v
_ 1a (m,m'a)-------->mm'a ma------------> mf(a)=f(ma)
φ f
Elienberg Moore Category による Resolution
二つのFunctor U^T, U^F そして、自然変換二つ η^T, μ^T を作ります。μ^T はμと同じですが型が違います。
U^T : Functor Eilenberg-MooreCategory A
U^T = record {
FObj = \a -> obj a
; FMap = \f -> EMap f
; isFunctor = record
{ ≈-cong = \eq -> eq
; identity = refl-hom
; distr = refl-hom
}
} where open ≈-Reasoning (A)
U^T は非常に簡単です。homoprphism を忘れるだけです。
F^T はそうはいきません。Algebra を構築していく必要があります。
open Monad
Lemma-EM4 : (x : Obj A ) -> A [ A [ TMap μ x o TMap η (FObj T x) ] ≈ id1 A (FObj T x) ]
Lemma-EM4 x = let open ≈-Reasoning (A) in
begin
TMap μ x o TMap η (FObj T x)
≈⟨ IsMonad.unity1 (isMonad M) ⟩
id1 A (FObj T x)
∎
Lemma-EM5 : (x : Obj A ) -> A [ A [ ( TMap μ x) o TMap μ (FObj T x) ] ≈ A [ ( TMap μ x) o FMap T ( TMap μ x) ] ]
Lemma-EM5 x = let open ≈-Reasoning (A) in
begin
( TMap μ x) o TMap μ (FObj T x)
≈⟨ IsMonad.assoc (isMonad M) ⟩
( TMap μ x) o FMap T ( TMap μ x)
∎
ftobj : Obj A -> EMObj
ftobj = \x -> record { a = FObj T x ; phi = TMap μ x;
isAlgebra = record {
identity = Lemma-EM4 x;
eval = Lemma-EM5 x
} }
FObj F^R では、Monad 則が、そのまま Obj に張り付くことがわかります。φ には μ(x) が入ります。
Lemma-EM6 : (a b : Obj A ) -> (f : Hom A a b ) ->
A [ A [ (φ (ftobj b)) o FMap T (FMap T f) ] ≈ A [ FMap T f o (φ (ftobj a)) ] ]
Lemma-EM6 a b f = let open ≈-Reasoning (A) in
begin
(φ (ftobj b)) o FMap T (FMap T f)
≈⟨⟩
TMap μ b o FMap T (FMap T f)
≈⟨ sym (nat μ) ⟩
FMap T f o TMap μ a
≈⟨⟩
FMap T f o (φ (ftobj a))
∎
Lemma-EM6 : (a b : Obj A ) -> (f : Hom A a b ) ->
A [ A [ (φ (ftobj b)) o FMap T (FMap T f) ] ≈ A [ FMap T f o (φ (ftobj a)) ] ]
Lemma-EM6 a b f = let open ≈-Reasoning (A) in
begin
(φ (ftobj b)) o FMap T (FMap T f)
≈⟨⟩
TMap μ b o FMap T (FMap T f)
≈⟨ sym (nat μ) ⟩
FMap T f o TMap μ a
≈⟨⟩
FMap T f o (φ (ftobj a))
∎
ftmap : {a b : Obj A} -> (Hom A a b) -> EMHom (ftobj a) (ftobj b)
ftmap {a} {b} f = record { EMap = FMap T f; homomorphism = Lemma-EM6 a b f }
FMap F^T では、μの可換性が homorphism になります。対象と射に Monad の要素が Algebra として付加されるわけです。それを除けば、F^T は実は T そのものです。実際、射の性質は、全部 T の性質にになります。
F^T : Functor A Eilenberg-MooreCategory
F^T = record {
FObj = ftobj
; FMap = ftmap
; isFunctor = record {
≈-cong = ≈-cong
; identity = identity
; distr = distr1
}
} where
≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → (ftmap f) ≗ (ftmap g)
≈-cong = let open ≈-Reasoning (A) in ( fcong T )
identity : {a : Obj A} → ftmap (id1 A a) ≗ EM-id {ftobj a}
identity = IsFunctor.identity ( isFunctor T )
distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → ftmap (A [ g o f ]) ≗ ( ftmap g ∙ ftmap f )
distr1 = let open ≈-Reasoning (A) in ( distr T )
U^T は制約を忘れる、F^T は制約を付加する T なわけですから、T = (U^T ○ F^T) が成立します。
Lemma-EM7 : ∀{a b : Obj A} -> (f : Hom A a b ) -> A [ FMap T f ≈ FMap (U^T ○ F^T) f ]
Lemma-EM7 {a} {b} f = let open ≈-Reasoning (A) in
sym ( begin
FMap (U^T ○ F^T) f
≈⟨⟩
EMap ( ftmap f )
≈⟨⟩
FMap T f
∎ )
Lemma-EM8 : T ≃ (U^T ○ F^T)
Lemma-EM8 f = Category.Cat.refl (Lemma-EM7 f)
証明というよりは定義から自明ですね。
自然変換を作る
η^T はηの型を変えたものです。EM7 で型を変換する必要があります。
η^T : NTrans A A identityFunctor ( U^T ○ F^T )
η^T = record { TMap = \x -> TMap η x ; isNTrans = isNTrans1 } where
commute1 : {a b : Obj A} {f : Hom A a b}
→ A [ A [ ( FMap ( U^T ○ F^T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ]
commute1 {a} {b} {f} = let open ≈-Reasoning (A) in
begin
( FMap ( U^T ○ F^T ) f ) o ( TMap η a )
≈⟨ sym (resp refl-hom (Lemma-EM7 f)) ⟩
FMap T f o TMap η a
≈⟨ nat η ⟩
TMap η b o f
∎
isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (\a -> TMap η a)
isNTrans1 = record { commute = commute1 }
本命はε^Tです。これは φ を取ってくる操作です。φは自然変換だったわけです。F^T が対象に付加した φ は自然変換 μ でした。homomorphism には eval を逆順入れます。これは F^T では Monad の assoc 則でした。
Lemma-EM9 : (a : EMObj) -> A [ A [ (φ a) o FMap T (φ a) ] ≈ A [ (φ a) o (φ (FObj ( F^T ○ U^T ) a)) ] ]
Lemma-EM9 a = let open ≈-Reasoning (A) in
sym ( begin
(φ a) o (φ (FObj ( F^T ○ U^T ) a))
≈⟨⟩
(φ a) o (TMap μ (obj a))
≈⟨ IsAlgebra.eval (isAlgebra a) ⟩
(φ a) o FMap T (φ a)
∎ )
emap-ε : (a : EMObj ) -> EMHom (FObj ( F^T ○ U^T ) a) a
emap-ε a = record { EMap = φ a ; homomorphism = Lemma-EM9 a }
ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor
ε^T = record { TMap = \a -> emap-ε a; isNTrans = isNTrans1 } where
commute1 : {a b : EMObj } {f : EMHom a b}
→ (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙( FMap (F^T ○ U^T) f ) )
commute1 {a} {b} {f} = let open ≈-Reasoning (A) in
sym ( begin
EMap (( emap-ε b ) ∙ ( FMap (F^T ○ U^T) f ))
≈⟨⟩
φ b o FMap T (EMap f)
≈⟨ homomorphism f ⟩
EMap f o φ a
≈⟨⟩
EMap (f ∙ ( emap-ε a ))
∎ )
isNTrans1 : IsNTrans Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (\a -> emap-ε a )
isNTrans1 = record { commute = \{a} {b} {f} ->
(IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A)) ) (homomorphism f ) } -- commute1 {a} {b} {f}
commute1 を使うと黄色くなってしまうので何かが足りないようです。 付加した制約が巧妙に、ε^T を構成していることがわかります。
μ^T は、いつもの通り、U^T ε^T F^T です。
emap-μ : (a : Obj A) -> Hom A (FObj ( U^T ○ F^T ) (FObj ( U^T ○ F^T ) a)) (FObj ( U^T ○ F^T ) a)
emap-μ a = FMap U^T ( TMap ε^T ( FObj F^T a ))
μ^T : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T )
μ^T = record { TMap = emap-μ ; isNTrans = isNTrans1 } where
commute1 : {a b : Obj A} {f : Hom A a b}
→ A [ A [ (FMap (U^T ○ F^T) f) o ( emap-μ a) ] ≈ A [ ( emap-μ b ) o FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) ] ]
commute1 {a} {b} {f} = let open ≈-Reasoning (A) in
sym ( begin
( emap-μ b ) o FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f)
≈⟨⟩
(FMap U^T ( TMap ε^T ( FObj F^T b ))) o (FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) )
≈⟨⟩
(TMap μ b) o (FMap T (FMap T f))
≈⟨ sym (nat μ) ⟩
FMap T f o ( TMap μ a )
≈⟨⟩
(FMap (U^T ○ F^T) f) o ( emap-μ a)
∎ )
isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ
isNTrans1 = record { commute = commute1 }
これが μと等しいことを示しておく必要があります。
Lemma-EM10 : {x : Obj A } -> A [ TMap μ^T x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
Lemma-EM10 {x} = let open ≈-Reasoning (A) in
sym ( begin
FMap U^T ( TMap ε^T ( FObj F^T x ) )
≈⟨⟩
emap-μ x
≈⟨⟩
TMap μ^T x
∎ )
Lemma-EM11 : {x : Obj A } -> A [ TMap μ x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ]
Lemma-EM11 {x} = let open ≈-Reasoning (A) in
sym ( begin
FMap U^T ( TMap ε^T ( FObj F^T x ) )
≈⟨⟩
TMap μ x
∎ )
証明と言うよりは単なる cast ですね。しかし、これを MResolution 側では示すことはできません。
Adjunction の構成
Adjoint の証明自体は短いものです。
Adj^T : Adjunction A Eilenberg-MooreCategory U^T F^T η^T ε^T
Adj^T = record {
isAdjunction = record {
adjoint1 = \{b} -> IsAlgebra.identity (isAlgebra b) ; -- adjoint1
adjoint2 = adjoint2
}
} where
adjoint1 : { b : EMObj } →
A [ A [ ( FMap U^T ( TMap ε^T b)) o ( TMap η^T ( FObj U^T b )) ] ≈ id1 A (FObj U^T b) ]
adjoint1 {b} = let open ≈-Reasoning (A) in
begin
( FMap U^T ( TMap ε^T b)) o ( TMap η^T ( FObj U^T b ))
≈⟨⟩
φ b o TMap η (obj b)
≈⟨ IsAlgebra.identity (isAlgebra b) ⟩
id1 A (a b)
≈⟨⟩
id1 A (FObj U^T b)
∎
adjoint2 : {a : Obj A} →
Eilenberg-MooreCategory [ Eilenberg-MooreCategory [ ( TMap ε^T ( FObj F^T a )) o ( FMap F^T ( TMap η^T a )) ]
≈ id1 Eilenberg-MooreCategory (FObj F^T a) ]
adjoint2 {a} = let open ≈-Reasoning (A) in
begin
EMap (( TMap ε^T ( FObj F^T a )) ∙ ( FMap F^T ( TMap η^T a )) )
≈⟨⟩
TMap μ a o FMap T ( TMap η a )
≈⟨ IsMonad.unity2 (isMonad M) ⟩
EMap (id1 Eilenberg-MooreCategory (FObj F^T a))
∎
最後に Resolution を構成して終わりです。
open MResolution
Resolution^T : MResolution A Eilenberg-MooreCategory T U^T F^T {η^T} {ε^T} {μ^T} Adj^T
Resolution^T = record {
T=UF = Lemma-EM8;
μ=UεF = Lemma-EM11
}
Next : Elienberg-Moore圏による Conparison Functor