-- Group definitions
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Group.Defs
import Foundation

-- Operation graphs and carriers are sets. These predicates are the explicit
-- set-theoretic counterparts of algebraic interfaces.
predicate LeftCancellation (A op : Set) := ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, op(a, b) = op(a, c) → b = c
predicate RightCancellation (A op : Set) := ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, op(b, a) = op(c, a) → b = c
predicate CancelMagma (A op : Set) := IsMagma(A, op) ∧ (LeftCancellation(A, op) ∧ RightCancellation(A, op))
predicate CancelMonoid (A op unit : Set) := IsMonoid(A, op, unit) ∧ CancelMagma(A, op)
predicate IsInverse (A op unit a b : Set) := a ∈ A ∧ (b ∈ A ∧ (op(b, a) = unit ∧ op(a, b) = unit))