{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving, GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds #-}

-- |

-- Module      : OAlg.AbelianGroup.Proposition

-- Description : validity of abelian groups

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- validity of abelian groups.

module OAlg.AbelianGroup.Proposition
  ( prpAbelianGroups
  ) where

import OAlg.Prelude

import OAlg.Data.FinitelyPresentable

import OAlg.Entity.Natural
import OAlg.Entity.FinList
import OAlg.Entity.Slice

import OAlg.AbelianGroup.Definition
import OAlg.AbelianGroup.KernelsAndCokernels
import OAlg.AbelianGroup.Liftable

--------------------------------------------------------------------------------

-- prpAbelianGroups -


-- | validity for abelian groups.

prpAbelianGroups :: Statement
prpAbelianGroups :: Statement
prpAbelianGroups = String -> Label
Prp String
"AbelianGroups"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpAbHom
            , String -> Label
Label String
"isoSmithNormal" Label -> Statement -> Statement
:<=>: X AbGroup -> (AbGroup -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X AbGroup
forall x. XStandard x => X x
xStandard (Inv AbHom -> Statement
forall a. Validable a => a -> Statement
valid (Inv AbHom -> Statement)
-> (AbGroup -> Inv AbHom) -> AbGroup -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. AbGroup -> Inv AbHom
isoSmithNormal)
            , String -> Label
Label String
"kernels" Label -> Statement -> Statement
:<=>: Kernels N1 AbHom -> Statement
forall a. Validable a => a -> Statement
valid Kernels N1 AbHom
abhKernels
            , String -> Label
Label String
"cokernels liftable" Label -> Statement -> Statement
:<=>: (CokernelsG ConeLiftable Diagram N1 AbHom -> Statement
forall a. Validable a => a -> Statement
valid CokernelsG ConeLiftable Diagram N1 AbHom
abhCokernelsLftFreeG)
            , String -> Label
Label String
"splitable" Label -> Statement -> Statement
:<=>: X (SomeFreeSlice 'From AbHom)
-> (SomeFreeSlice 'From AbHom -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (N -> X (SomeFreeSlice 'From AbHom)
xAbhSomeFreeSlice N
100) (SomeFinList (Slice 'From (Free N1) AbHom) -> Statement
forall a. Validable a => a -> Statement
valid (SomeFinList (Slice 'From (Free N1) AbHom) -> Statement)
-> (SomeFreeSlice 'From AbHom
    -> SomeFinList (Slice 'From (Free N1) AbHom))
-> SomeFreeSlice 'From AbHom
-> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. SomeFreeSlice 'From AbHom
-> SomeFinList (Slice 'From (Free N1) AbHom)
abhSplit)
            , Statement
prpMatrixZLiftable
            ]
  where
    abhSplit :: SomeFreeSlice From AbHom -> SomeFinList (Slice From (Free N1) AbHom)
    abhSplit :: SomeFreeSlice 'From AbHom
-> SomeFinList (Slice 'From (Free N1) AbHom)
abhSplit (SomeFreeSlice Slice 'From (Free k) AbHom
hs) = FinList k (Slice 'From (Free N1) AbHom)
-> SomeFinList (Slice 'From (Free N1) AbHom)
forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList (FinList k (Slice 'From (Free N1) AbHom)
 -> SomeFinList (Slice 'From (Free N1) AbHom))
-> FinList k (Slice 'From (Free N1) AbHom)
-> SomeFinList (Slice 'From (Free N1) AbHom)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Splitable 'From Free AbHom
-> Slice 'From (Free k) AbHom
-> FinList k (Slice 'From (Free N1) AbHom)
forall (k :: N') (i :: N' -> * -> *) d (s :: Site).
(Attestable k, Sliced (i k) d) =>
Splitable s i d -> Slice s (i k) d -> FinList k (Slice s (i N1) d)
split Splitable 'From Free AbHom
abhSplitable Slice 'From (Free k) AbHom
hs