some progress on hom of abelian groups

Author: pierrecagne

abelian.tex

@@ -776,6 +776,60 @@ \subsection{Higher deloopings}
 Notice that where W\"arn's method shines, compared to our, is in
 producing further delooping $\B^n G$ for $n\geq 3$.
 
+\section{Homomorphisms of abelian groups}
+\label{sec:ab-hom}
+
+For concrete groups $G$ and $H$, we have defined the set $\Hom(G,H)$ of group
+homomorphisms from $G$ to $H$ as the set $\BG \ptdto \BH$. When the codomain $H$
+is abelian, it turns out that $\Hom(G,H)$ is an abstract abelian group. In this
+section, we define a concrete abelian group $\grpHom(G,H)$ with an identification
+$\Hom(G,H) = \US{\grpHom(G,H)}$.
+
+Given types $X,Y$ and a point $y:Y$, recall that $\cst y$ is the function that
+maps all $x:X$ to $y$. If $X$ and $Y$ are pointed, then the function $\cst
+{\pt_Y}$ is trivially pointed by $\refl{\pt_Y}$.
+
+\begin{definition}
+  Let $G$ and $H$ be concrete groups. Assume $H$ is abelian. Define
+  \begin{displaymath}
+    \grpHom(G,H) \defeq \Aut_{\BG \ptdto \BB H} (\cst {\pt_{\BB H}})
+  \end{displaymath}
+\end{definition}
+
+Notice that, since $\BB H$ is a 2-type, the type $\BG \ptdto \BB H$ is 1-type and thus $\grpHom(G,H)$ is well-defined.
+
+\begin{lemma}
+  Let $G$ and $H$ be abelian groups. There is a bijection of sets of type
+  \begin{displaymath}
+    \US{\grpHom(G,H)} \equivto \Hom(G,H).
+  \end{displaymath}
+\end{lemma} 
+\begin{proof}
+  We simply follow the chain of equivalences:
+  \begin{align*}
+    \US{\grpHom(G,H)}
+    &\defeq \cst {\pt_{\BB H}} \eqto \cst {\pt_{\BB H}}
+    \\
+    &\equivto \sum_{e : \prod_{x:\BG} \pt_{\BB H} \eqto \pt_{\BB H}} \refl{\pt_{\BB H}} = e ({\pt_{\BG}})
+    \\
+    &\equivto \sum_{e : \BG \to \BH} \sh_H = e ({\sh_G}) 
+    \\
+    &\equivto \Hom(G,H)
+  \end{align*}
+\end{proof}
+  
+Notice that the previous equivalence equips $\Hom(G,H)$ with the structure of an abstract group. Its unit is the image of the unit of $\grpHom(G,H)$, i.e.\ the constant homomorphism $\mkhom{\cst {\sh_H}}$. Its multiplication is the image of the multiplication of $\grpHom(G,H)$. To understand it better, we need to unfold how the composition of symmetries of $\cst {\pt_{\BB H}}$ translates through the first equivalence of the chain above. Given $p,q : \cst {\pt_{\BB H}} \eqto \cst {\pt_{\BB H}}$ with $p$ sent to the pair $(e,e_\ast)$ and $q$ to the pair $(f,f_\ast)$, the composition $p\cdot q$ is sent to the pair $(g,g_\ast)$ for which, for all $x:\BG$, there is a path $\alpha_x : g(x) = e(x) \cdot f(x)$ such that $g_\ast = \alpha_{\pt_{\BG}} \cdot (e_\ast \ast f_\ast)$ where $\ast$ is the horizontal composition. In other words, for $\phi,\psi:\Hom(G,H)$, their multiplication $\phi\psi$ comes together with $\alpha: \B (\phi\psi) \eqto \B \phi \cdot \B \psi$ where the right hand-side is the pointwise composition of path-valued pointed function. If we follow through with the bijection $\Hom(G,H) \equivto \absHom(G,H)$, then this equips $\absHom(G,H)$ with the pointwise group structure. 
+
+\begin{lemma}
+  Let $G$ and $H$ be abelian groups. There is a bijection of sets of type
+  \begin{displaymath}
+    \US{\grpHom(G,H)} \equivto (\BB G \ptdto \BB H).
+  \end{displaymath}
+\end{lemma}
+
+\section{The category of abelian groups}
+\label{sec:ab-mon-closed-cat}
+
 \section{Direct sums and reduced wreath products}
 \label{sec:direct-sums}
 

agda-test/abhom.agda

@@ -0,0 +1,122 @@
+
+{-# OPTIONS --cubical-compatible #-}
+
+module abhom where
+
+data _≡_ {A : Set} (a : A) : A → Set where
+  refl : a ≡ a
+
+trp : ∀ {A} {B : A → Set} {a₁ a₂ : A} → (a₁ ≡ a₂) → B a₁ → B a₂
+trp refl b = b
+
+_∙_ : ∀ {A} {a₁ a₂ a₃ : A} → (a₂ ≡ a₃) → (a₁ ≡ a₂) → (a₁ ≡ a₃)
+
+p ∙ refl = p
+
+refl∙ : ∀ {A} {a₁ a₂ : A} {p : a₁ ≡ a₂} → p ≡ (refl ∙ p)
+refl∙ {p = refl} = refl
+
+[_] : ∀ {A B} {a₁ a₂ : A} (f : A → B) → (a₁ ≡ a₂) → (f a₁) ≡ (f a₂)  
+[ f ] refl = refl 
+
+module ≡-Reasoning {A : Set} where
+
+  infix  1 begin_
+  infixr 2 step-≡-∣ step-≡-⟩
+  infix  3 _∎
+
+  begin_ : ∀ {x y : A} → x ≡ y → x ≡ y
+  begin x≡y  =  x≡y
+
+  step-≡-∣ : ∀ (x : A) {y : A} → x ≡ y → x ≡ y
+  step-≡-∣ x x≡y  =  x≡y
+
+  step-≡-⟩ : ∀ (x : A) {y z : A} → y ≡ z → x ≡ y → x ≡ z
+  step-≡-⟩ x y≡z x≡y  = y≡z ∙ x≡y
+
+  syntax step-≡-∣ x x≡y      =  x ≡⟨⟩ x≡y
+  syntax step-≡-⟩ x y≡z x≡y  =  x ≡⟨  x≡y ⟩ y≡z
+
+  _∎ : ∀ (x : A) → x ≡ x
+  x ∎  =  refl
+
+open ≡-Reasoning
+
+η≡ : ∀ {A B : Set} {f g : A → B} → (f ≡ g) → ∀ x → (f x) ≡ (g x)
+η≡ refl x = refl
+
+postulate fun-ext : ∀ {A B : Set} {f g : A → B} → (∀ x → (f x) ≡ (g x)) → (f ≡ g)
+
+η≡-∙ : ∀ {A B : Set} {f g h : A → B} (p : g ≡ h) (q : f ≡ g) → ∀ x → η≡ (p ∙ q) x ≡ ((η≡ p x) ∙ (η≡ q x))
+η≡-∙ refl refl x = refl
+
+isProp : Set → Set
+isProp A = ∀ (x y : A) → x ≡ y 
+
+isSet : Set → Set
+isSet A = ∀ (x y : A) → isProp (x ≡ y)
+
+isGrpd : Set →  Set
+isGrpd A = ∀ (x y : A) → isSet (x ≡ y)
+
+is2Type : Set → Set
+is2Type A = ∀ (x y : A) → isGrpd (x ≡ y)
+
+data Σ (A : Set) (B : A → Set) : Set where
+  _,_ : ∀ a → B a → Σ A B 
+
+fst : ∀ {A B} → Σ A B → A
+fst (x , y) = x
+
+snd : ∀ {A B} → ∀ (p : Σ A B) → B (fst p)
+snd (x , y) = y
+
+Σ≡ : ∀ {A B} {x y : Σ A B} → x ≡ y → Σ ((fst x) ≡ (fst y)) (λ p → (snd y) ≡ (trp {B = B} p (snd x)))
+Σ≡ refl = refl , refl
+
+≡Σ : ∀ {A B} {x y : Σ A B} (p : (fst x) ≡ (fst y)) → (snd y) ≡ (trp {B = B} p (snd x)) → x ≡ y
+≡Σ {x = x₁ , x₂} {y = y₁ , y₂} refl refl = refl
+
+Ω : ∀ A → A → Set
+Ω A a = a ≡ a
+
+ptdMap : ∀ A (a : A) B (b : B) → Set
+ptdMap A a B b = Σ (A → B) λ f → b ≡ (f a)
+
+cst⋆ : ∀ A (a : A) B (b : B) → ptdMap A a B b
+cst⋆ A a B b = (λ _ → b) , refl
+
+ptw-∙ : ∀ {A B a b} → ptdMap A a (Ω B b) refl → ptdMap A a (Ω B b) refl → ptdMap A a (Ω B b) refl
+ptw-∙ {a = a} (f , f⋆) (g , g⋆) = (λ x → f x ∙ g x) ,  ([ _∙_ (f a) ] g⋆ ∙ f⋆) -- (([ (λ p → p ∙ (g a)) ] f⋆) ∙ [ (λ p → refl ∙ p) ] g⋆)
+
+≡-pdtMap : ∀ {A} {a : A} {B} {b : B} {f g : ptdMap A a B b} (p : f ≡ g) → (snd g) ≡ ((η≡ (fst (Σ≡ p)) a) ∙ (snd f))
+≡-pdtMap refl = refl∙
+
+trp-pdtMap : ∀ {A} {a : A} {B} {b : B} {f g : A → B} (p : f ≡ g) (q : b ≡ f a) → (trp p q) ≡ (η≡ p a ∙ q)
+trp-pdtMap refl q = refl∙
+
+≡-pdtMap-∙ : ∀ {A} {a : A} {B} {b : B} {f g h : ptdMap A a B b} (p : g ≡ h) (q : f ≡ g) → (fst (Σ≡ (p ∙ q))) ≡ ((fst (Σ≡ p)) ∙ (fst (Σ≡ q)))
+≡-pdtMap-∙ refl refl = refl
+
+
+trp-≡-ptdMap-∙ : ∀ {A} {a : A} {B} {b : B} {f g h : ptdMap A a B b} (p : g ≡ h) (q : f ≡ g)
+   → ([ _∙_ (η≡ (fst (Σ≡ p)) a) ] (≡-pdtMap q) ∙ ≡-pdtMap p)
+   ≡ (trp {A = A → Ω B }  ({!fun-ext!} ∙ ([ η≡ ] (≡-pdtMap-∙ p q))) (≡-pdtMap (p ∙ q)))
+trp-≡-ptdMap-∙ = {!!}
+
+abHom : ∀ BG shG B²H pt-B²H → Ω (ptdMap BG shG B²H pt-B²H) (cst⋆ BG shG B²H pt-B²H) → ptdMap BG shG (Ω B²H pt-B²H) refl  
+abHom BG shG B²H pt-B²H p = (η≡ (fst (Σ≡ p))) , (≡-pdtMap p)
+--with Σ≡ p
+--... | p₁ , p₂ = (η≡ p₁) , (trp-pdtMap p₁ refl ∙ p₂)
+
+abHom-unit : ∀ BG shG B²H pt-B²H → (abHom BG shG B²H pt-B²H) refl ≡ (cst⋆ BG shG (Ω B²H pt-B²H) refl)
+abHom-unit BG shG B²H pt-B²H = refl
+
+abHom-mult : ∀ BG shG B²H pt-B²H p q → (abHom BG shG B²H pt-B²H) (p ∙ q) ≡ ptw-∙ (abHom BG shG B²H pt-B²H p) (abHom BG shG B²H pt-B²H q)
+abHom-mult BG shG B²H pt-B²H p q =  ≡Σ (fun-ext (η≡-∙ (fst (Σ≡ p)) (fst (Σ≡ q))) ∙ ([ η≡ ] (≡-pdtMap-∙ p q))) {!(fun-ext (η≡-∙ (fst (Σ≡ p)) (fst (Σ≡ q))) ∙
+ [ η≡ ] (≡-pdtMap-∙ p q))!}
+--with Σ≡ p | Σ≡ q
+--... | p- , p⋆ | q- , q⋆ = ≡Σ ( fun-ext (η≡-∙ p- q-) ∙ {![ η≡ ] ?!} ) {!!}
+
+
+