Algebra contributions

[LionOfJewdah]

I have some ideas I'd like to contribute to stdlib Algebra (beyond just matrices, #3101). I was thinking perhaps the induced subgroup theorem and perhaps things like group/ring completion:

Induced subgroup theorem

(And generalizations to monoids and rings, etc) which basically given

module _ (G : Group c ℓ) where
  open Group G

  record IsSubgroupPredicate (P : Pred Carrier ℓ₁) : Set _ where
    field
      id-closed  : P ε
      mul-closed : ∀ {x y} → P x → P y → P (x ∙ y)
      inv-closed : ∀ {x}   → P x     → P (x ⁻¹)

     SubCarrier : Set (c ⊔ ℓ₁)
     SubCarrier = Σ Carrier P

you construct the induced subgroup (/submonoid/subring), you can transitively chain them, and even construct homomorphism kernels (e.g. KernelPred x = f x H.≈ H.ε, for f a homomorphism G → H)

Group completion and similar

The easiest place to start is commutative monoids completed as Abelian groups. Basically,

open CommutativeMonoid M renaming ( _∙_ to _+_; ε to 0# ) -- etc

infix 8 _⊝_
record Difference : Set ℓ where
  constructor _⊝_
  field
    credit : Carrier
    debit  : Carrier

open Difference public

infix 4 _≈ᵍ_
record _≈ᵍ_ (p q : Difference) : Set (ℓ ⊔ ℓeq) where
  constructor equals
  field
    slack    : Carrier
    balanced : ((credit p + debit q) + slack) ≈ ((credit q + debit p) + slack)

The slack is necessary because the naive relation a + d ≈ c + b is transitive only when the monoid is cancellative; so it needs to have no idempotents. This can be done with non-commutative monoids, and with semirings to rings, and (trivially) semigroups to monoids (adjoin an identity; if there is already ε; it is setoidally equal to the adjoined one). If you start with a non-cancellative monoid or semiring, you get the trivial group or ring; for example, if we start with [0, +∞) we could get things that preclude negatives like "4 + ∞ = ∞; so -(4 + ∞) = -∞ so ∞ - ∞ = 0; but 2 + ∞ = ∞ so -(2 + ∞) = -∞ so ∞ - ∞ = (4 + ∞) - (2 + ∞) = 2 ≠ 0".

[jamesmckinna]

Discussions has recently opened as a place to collect together 'higher level' topics around the current design of the standard library, and of libraries in general, in the context of a large scale overhaul being undertaken towards v3.0.

Suggest that if you're interested in making a concrete contribution to the existing library, then rather than post here, that you open a pull request. When doing so, please make sure to read HACKING, as well as doc/style-guide, as well as looking at existing open issues and PRs on related topics, such as #2891