Module mathcomp.boot.monoid
From HB Require Import structures.From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
From mathcomp Require Import bigop fintype finfun.
Group-like structures
NB: See CONTRIBUTING.md for an introduction to HB concepts and commands.
This file defines the following algebraic structures:
magmaType == magma
The HB class is called Magma.
ChoiceMagma.type == join of magmaType and choiceType
The HB class is called ChoiceMagma.
semigroupType == associative magma
The HB class is called Semigroup.
baseUMagmaType == pointed magma
The HB class is called BaseUMagma.
ChoiceBaseUMagma.type == join of baseUMagmaType and choiceType
The HB class is called ChoiceBaseUMagma.
umagmaType == unitary magma
The HB class is called UMagma.
monoidType == monoid
The HB class is called Monoid.
baseGroupType == pointed magma with an inversion operator
The HB class is called BaseGroup.
starMonoidType == *-monoid, i.e. monoid with an involutive
antiautomorphism
The HB class is called BaseGroup.
groupType == group
The HB class is called Group.
and their joins with subType:
subMagmaType V P == join of magmaType and subType (P : pred V) such
that val is multiplicative
The HB class is called SubMagma.
subSemigroupType V P == join of semigroupType and subType (P : pred V)
such that val is multiplicative
The HB class is called SubSemigroup.
subBaseUMagmaType V P == join of baseUMagmaType and subType (P : pred V)
such that val is multiplicative and preserves 1
The HB class is called SubBaseUMagma.
subUMagmaType V P == join of UMagmaType and subType (P : pred V)
such that val is multiplicative and preserves 1
The HB class is called SubUMagma.
subMonoidType V P == join of monoidType and subType (P : pred V)
such that val is multiplicative and preserves 1
The HB class is called SubMonoid.
subGroupType V P == join of groupType and subType (P : pred V)
such that val is multiplicative and preserves 1
The HB class is called SubGroup.
Morphisms between the above structures:
Multiplicative.type G H == multiplicative functions between magmaType
instances G and H
UMagmaMorphism.type G H == multiplicative functions preserving 1 between
baseUMagmaType instances G and H
Closedness predicates for the algebraic structures:
mulgClosed V == predicate closed under multiplication on G : magmaType
The HB class is called MulClosed.
umagmaClosed V == predicate closed under multiplication and containing 1
on G : baseUMagmaType
The HB class is called UMagmaClosed.
invgClosed V == predicate closed under inversion on G : baseGroupType
The HB class is called InvClosed.
groupClosed V == predicate closed under multiplication and inversion and
containing 1 on G : baseGroupType
The HB class is called InvClosed.
Canonical properties of the algebraic structures:
* magmaType (magmas):
x * y == the product of x and y
commute x y <-> x and y commute (i.e. x * y = y * x)
mulg_closed S <-> collective predicate S is closed under
multiplication
* baseUMagmaType (pointed magmas):
1 == the unit of a unitary magma
x ^+ n == x to the power n, with n in nat (non-negative),
i.e. x * (x * .. (x * x)..) (n terms); x ^+ 1 is
thus convertible to x, and x ^+ 2 to x * x
\prod<range> e == iterated product for a baseUMagmaType (cf bigop.v)
umagma_closed S <-> collective predicate S is closed under
multiplication and contains 1
* monoidType (monoids):
monoid_closed S := umagma_closed S
* baseGroupType (pointed magmas with an inversion operator):
x ^-1 == the inverse of x
x / y == x * (y ^- 1)
x ^- n == (x ^+ n)^-1
x ^ y := y^-1 * (x * y)
== the conjugate of x by y
[~ x, y] := x^-1 * (y^-1 * (x * y)
== the commutator of x and y
invg_closed S <-> collective predicate S is closed under inversion
divg_closed S <-> collective predicate S is closed under division
group_closed S <-> collective predicate S is closed under division
and contains 1
In addition to this structure hierarchy, we also develop a separate,
* Multiplicative (magma morphisms):
{multiplicative U -> V} == the interface type for magma morphisms, i.e.
functions from U to V which maps * in U to * in
V; both U and V must have magmaType instances
:= GRing.RMorphism.type R S
* UMagmaMorphism (unitary magma morphisms):
monoid_morphism f <-> f of type U -> V is a multiplicative monoid
morphism, i.e., f maps 1 and * in U to 1 and
* in V, respectively. U and V must have
canonical baseUMagmaType instances.
(*Algebra.UMagmaMorphism.type == the interface type for unitary magma
morphisms; both U and V must have magmaType
instances
Notations are defined in scope group_scope (delimiter %g)
This library also extends the conventional suffixes described in library
ssrbool.v with the following:
1 -- unitary magma 1, as in mulg1 : x * 1 = x
M -- magma multiplication, as in conjgM : x ^ (y * z) = (x ^ y) ^ z
Mn -- ring by nat multiplication, as in expgMn :
(x * y) ^+ n = x ^+ n * y ^+ n
V -- group inverse, as in expVgn : (x^-1) ^+ n = x ^- n
F -- group division, as in invgF : (x / y)^-1 = y / x
X -- unitary magma exponentiation, as in conjXg :
(x ^+ n) ^ y = (x ^ y) ^+ n
J -- group conjugation, as in conjJg : (x ^ y) ^ z = (x ^ z) ^ y ^ z
R -- group commutator, as in conjRg : [~ x, y] ^ z = [~ x ^ z, y ^ z]
The operator suffixes D, B, M and X are also used for the corresponding
operations on nat, as in expgnDr : x ^+ (m + n) = x ^+ m * x ^+ n. For the
binary power operator, a trailing "n" suffix is used to indicate the
operator suffix applies to the left-hand group argument, as in
expg1n : 1 ^+ n = 1 vs. expg1 : x ^+ 1 = x.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Reserved Notation "*%g" (at level 0).
Reserved Notation "\1" (at level 0).
Reserved Notation "f \* g" (at level 40, left associativity).
Reserved Notation "'{' 'multiplicative' G '->' H '}'"
(at level 0, G at level 98, H at level 99,
format "{ 'multiplicative' G -> H }").
Declare Scope group_scope.
Delimit Scope group_scope with g.
Local Open Scope group_scope.
HB.mixin Record hasMul G := {
mul : G -> G -> G
}.
#[short(type="magmaType")]
HB.structure Definition Magma := {G of hasMul G}.
Bind Scope group_scope with Magma.sort.
HB.structure Definition ChoiceMagma := {G of Magma G & Choice G}.
Bind Scope group_scope with ChoiceMagma.sort.
Local Notation "*%g" := (@mul _) : function_scope.
Local Notation "x * y" := (mul x y) : group_scope.
Section MagmaTheory.
Variable G : magmaType.
Implicit Types x y : G.
Definition commute x y := x * y = y * x.
Lemma commute_refl x : commute x x.
Proof.
by []. Qed.
Lemma commute_sym x y : commute x y -> commute y x.
Proof.
by []. Qed.
Section ClosedPredicates.
Variable S : {pred G}.
Definition mulg_closed := {in S &, forall u v, u * v \in S}.
End ClosedPredicates.
End MagmaTheory.
Prenex Implicits commute.
HB.mixin Record Magma_isSemigroup G & Magma G := {
mulgA : associative (@mul G)
}.
#[short(type="semigroupType")]
HB.structure Definition Semigroup := {G of Magma_isSemigroup G & ChoiceMagma G}.
HB.factory Record isSemigroup G & Choice G := {
mul : G -> G -> G;
mulgA : associative mul
}.
HB.builders Context G & isSemigroup G.
HB.instance Definition _ := hasMul.Build G mul.
HB.instance Definition _ := Magma_isSemigroup.Build G mulgA.
HB.end.
Bind Scope group_scope with Semigroup.sort.
Section SemigroupTheory.
Variable G : semigroupType.
Implicit Types x y : G.
#[export]
HB.instance Definition _ := SemiGroup.isLaw.Build G *%g mulgA.
Lemma commuteM x y z : commute x y -> commute x z -> commute x (y * z).
End SemigroupTheory.
HB.mixin Record hasOne G := {
one : G
}.
#[short(type="baseUMagmaType")]
HB.structure Definition BaseUMagma := {G of hasOne G & Magma G}.
Bind Scope group_scope with BaseUMagma.sort.
HB.structure Definition ChoiceBaseUMagma := {G of BaseUMagma G & Choice G}.
Bind Scope group_scope with ChoiceBaseUMagma.sort.
Local Notation "1" := (@one _) : group_scope.
Local Notation "s `_ i" := (nth 1 s i) : group_scope.
Local Notation "\prod_ ( i <- r | P ) F" := (\big[*%g/1]_(i <- r | P) F).
Local Notation "\prod_ ( i | P ) F" := (\big[*%g/1]_(i | P) F).
Local Notation "\prod_ ( i 'in' A ) F" := (\big[*%g/1]_(i in A) F).
Local Notation "\prod_ ( m <= i < n ) F" := (\big[*%g/1%g]_(m <= i < n) F%g).
Definition natexp (G : baseUMagmaType) (x : G) n : G := iterop n *%g x 1.
Arguments natexp : simpl never.
Local Notation "x ^+ n" := (natexp x n) : group_scope.
Section baseUMagmaTheory.
Variable G : baseUMagmaType.
Implicit Types x : G.
Lemma expgnE x n : x ^+ n = iterop n mul x 1
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma expgSS x n : x ^+ n.+2 = x * x ^+ n.+1.
Proof.
by []. Qed.
Lemma expgb x (b : bool) : x ^+ b = (if b then x else 1).
Proof.
by case: b. Qed.
Section ClosedPredicates.
Variable S : {pred G}.
Definition umagma_closed := 1 \in S /\ mulg_closed S.
End ClosedPredicates.
End baseUMagmaTheory.
HB.mixin Record BaseUMagma_isUMagma G & BaseUMagma G := {
mul1g : left_id one (@mul G);
mulg1 : right_id one (@mul G)
}.
HB.factory Record Magma_isUMagma G & Magma G := {
one : G;
mul1g : left_id one (@mul G);
mulg1 : right_id one (@mul G)
}.
HB.builders Context G & Magma_isUMagma G.
HB.instance Definition _ := hasOne.Build G one.
#[warning="-HB.no-new-instance"]
HB.instance Definition _ := BaseUMagma_isUMagma.Build G mul1g mulg1.
HB.end.
#[short(type="umagmaType")]
HB.structure Definition UMagma := {G of Magma_isUMagma G & ChoiceMagma G}.
Bind Scope group_scope with UMagma.sort.
Section UMagmaTheory.
Variable G : umagmaType.
Implicit Types x y : G.
Lemma expgS x n : x ^+ n.+1 = x * x ^+ n.
Proof.
Lemma expg1n n : 1 ^+ n = 1 :> G.
Lemma commute1 x : commute x 1.
End UMagmaTheory.
#[global] Hint Resolve commute1 : core.
#[short(type="monoidType")]
HB.structure Definition Monoid := {G of Magma_isUMagma G & Semigroup G}.
HB.factory Record Semigroup_isMonoid G & Semigroup G := {
one : G;
mul1g : left_id one mul;
mulg1 : right_id one mul
}.
HB.builders Context G & Semigroup_isMonoid G.
HB.instance Definition _ := Magma_isUMagma.Build G mul1g mulg1.
HB.end.
HB.factory Record UMagma_isMonoid G & UMagma G := {
mulgA : associative (@mul G)
}.
HB.builders Context G & UMagma_isMonoid G.
HB.instance Definition _ := Magma_isSemigroup.Build G mulgA.
HB.end.
HB.factory Record isMonoid G & Choice G := {
mul : G -> G -> G;
one : G;
mulgA : associative mul;
mul1g : left_id one mul;
mulg1 : right_id one mul
}.
HB.builders Context G & isMonoid G.
HB.instance Definition _ := hasMul.Build G mul.
HB.instance Definition _ := Magma_isSemigroup.Build G mulgA.
HB.instance Definition _ := Magma_isUMagma.Build G mul1g mulg1.
HB.end.
#[export]
HB.instance Definition _ (G : monoidType) :=
Monoid.isMonoidLaw.Build G 1 *%g mul1g mulg1.
Bind Scope group_scope with Monoid.sort.
Section MonoidTheory.
Variable G : monoidType.
Implicit Types x y : G.
Lemma expgnDr x m n : x ^+ (m + n) = x ^+ m * x ^+ n.
Lemma expgSr x n : x ^+ n.+1 = x ^+ n * x.
Lemma expgnA x m n : x ^+ (m * n) = x ^+ m ^+ n.
Lemma expgnAC x m n : x ^+ m ^+ n = x ^+ n ^+ m.
Lemma iter_mulg n x y : iter n ( *%g x) y = x ^+ n * y.
Lemma iter_mulg_1 n x : iter n ( *%g x) 1 = x ^+ n.
Lemma prodg_const (I : finType) (A : pred I) x : \prod_(i in A) x = x ^+ #|A|.
Lemma prodg_const_nat n m x : \prod_(n <= i < m) x = x ^+ (m - n).
Proof.
Lemma prodgXr x I r P (F : I -> nat) :
\prod_(i <- r | P i) x ^+ F i = x ^+ (\sum_(i <- r | P i) F i).
Lemma commute_prod (I : Type) (s : seq I) (P : pred I) (F : I -> G) x :
(forall i, P i -> commute x (F i)) -> commute x (\prod_(i <- s | P i) F i).
Lemma prodgM_commute {I : eqType} r (P : pred I) (F H : I -> G) :
(forall i j, P i -> P j -> commute (F i) (H j)) ->
\prod_(i <- r | P i) (F i * H i) =
\prod_(i <- r | P i) F i * \prod_(i <- r | P i) H i.
Proof.
move=> FH; elim: r => [|i r IHr]; rewrite !(big_nil, big_cons) ?mulg1//.
case: ifPn => // Pi; rewrite IHr !mulgA; congr (_ * _); rewrite -!mulgA.
by rewrite commute_prod // => j Pj; apply/commute_sym/FH.
Qed.
case: ifPn => // Pi; rewrite IHr !mulgA; congr (_ * _); rewrite -!mulgA.
by rewrite commute_prod // => j Pj; apply/commute_sym/FH.
Qed.
Lemma prodgMl_commute {I : finType} (A : pred I) (x : G) F :
(forall i, A i -> commute x (F i)) ->
\prod_(i in A) (x * F i) = x ^+ #|A| * \prod_(i in A) F i.
Proof.
Lemma prodgMr_commute {I : finType} (A : pred I) (x : G) F :
(forall i, A i -> commute x (F i)) ->
\prod_(i in A) (F i * x) = \prod_(i in A) F i * x ^+ #|A|.
Proof.
Lemma commuteX x y n : commute x y -> commute x (y ^+ n).
Lemma commuteX2 x y m n : commute x y -> commute (x ^+ m) (y ^+ n).
Proof.
Lemma expgMn x y n : commute x y -> (x * y) ^+ n = x ^+ n * y ^+ n.
Proof.
End MonoidTheory.
Notation monoid_closed := umagma_closed.
HB.mixin Record hasInv G := {
inv : G -> G
}.
#[short(type="baseGroupType")]
HB.structure Definition BaseGroup := {G of hasInv G & BaseUMagma G}.
Bind Scope group_scope with BaseGroup.sort.
Local Notation "x ^-1" := (inv x) : group_scope.
Local Notation "x / y" := (x * y^-1) : group_scope.
Local Notation "x ^- n" := ((x ^+ n)^-1) : group_scope.
Definition conjg (G : baseGroupType) (x y : G) := y^-1 * (x * y).
Local Notation "x ^ y" := (conjg x y) : group_scope.
Definition commg (G : baseGroupType) (x y : G) := x^-1 * (conjg x y).
Local Notation "[ ~ x1 , x2 , .. , xn ]" := (commg .. (commg x1 x2) .. xn)
: group_scope.
Section ClosedPredicates.
Variable (G : baseGroupType) (S : {pred G}).
Definition invg_closed := {in S, forall u, u^-1 \in S}.
Definition divg_closed := {in S &, forall u v, u / v \in S}.
Definition group_closed := 1 \in S /\ divg_closed.
End ClosedPredicates.
HB.mixin Record Monoid_isStarMonoid G & BaseGroup G := {
invgK : involutive (@inv G);
invgM : {morph @inv G : x y / x * y >-> y * x}
}.
#[short(type="starMonoidType")]
HB.structure Definition StarMonoid :=
{ G of Monoid_isStarMonoid G & Monoid G & BaseGroup G }.
Prenex Implicits invgK.
Bind Scope group_scope with StarMonoid.sort.
HB.factory Record isStarMonoid G & Choice G := {
mul : G -> G -> G;
one : G;
inv : G -> G;
mulgA : associative mul;
mul1g : left_id one mul;
invgK : involutive inv;
invgM : {morph inv : x y / mul x y >-> mul y x}
}.
HB.builders Context G & isStarMonoid G.
Lemma invg1 : inv one = one.
Lemma mulg1 : right_id one mul.
HB.instance Definition _ := isMonoid.Build G mulgA mul1g mulg1.
HB.instance Definition _ := hasInv.Build G inv.
HB.instance Definition _ := Monoid_isStarMonoid.Build G invgK invgM.
HB.end.
Section StarMonoidTheory.
Variable G : starMonoidType.
Implicit Types x y z : G.
Lemma invg_inj : injective (@inv G)
Lemma invg1 : 1^-1 = 1 :> G.
Lemma invgF x y : (x / y)^-1 = y / x.
Lemma prodgV I r (P : pred I) (E : I -> G) :
\prod_(i <- r | P i) (E i)^-1 = (\prod_(i <- rev r | P i) E i)^-1.
Proof.
Lemma eqg_inv x y : (x^-1 == y^-1) = (x == y).
Lemma eqg_invLR x y : (x^-1 == y) = (x == y^-1).
Lemma invg_eq1 x : (x^-1 == 1) = (x == 1).
Lemma expVgn x n : x^-1 ^+ n = x ^- n.
Lemma conjgE x y : x ^ y = y^-1 * (x * y)
Proof.
by []. Qed.
Lemma commgEl x y : [~ x, y] = x^-1 * x ^ y
Proof.
by []. Qed.
Lemma commgEr x y : [~ x, y] = y^-1 ^ x * y.
Proof.
End StarMonoidTheory.
Arguments invg_inj {G} [x1 x2].
HB.mixin Record StarMonoid_isGroup G & BaseGroup G := {
mulVg : left_inverse one inv (@mul G);
}.
#[short(type="groupType")]
HB.structure Definition Group :=
{G of StarMonoid_isGroup G & BaseGroup G & StarMonoid G}.
HB.factory Record Monoid_isGroup G & Monoid G & BaseGroup G := {
mulVg : left_inverse one inv (@mul G);
mulgV : right_inverse one inv (@mul G);
}.
HB.builders Context G & Monoid_isGroup G.
Fact invgK : involutive (@inv G).
Fact mulKg : @left_loop G G inv *%g.
Fact invgM : {morph inv : x y / x * y >-> y * x : G}.
Proof.
HB.instance Definition _ := Monoid_isStarMonoid.Build G invgK invgM.
HB.instance Definition _ := StarMonoid_isGroup.Build G mulVg.
HB.end.
HB.factory Record isGroup G & Choice G := {
one : G;
inv : G -> G;
mul : G -> G -> G;
mulgA : associative mul;
mul1g : left_id one mul;
mulg1 : right_id one mul;
mulVg : left_inverse one inv mul;
mulgV : right_inverse one inv mul
}.
HB.builders Context G & isGroup G.
HB.instance Definition _ := hasMul.Build G mul.
HB.instance Definition _ := Magma_isSemigroup.Build G mulgA.
HB.instance Definition _ := Magma_isUMagma.Build G mul1g mulg1.
HB.instance Definition _ := hasInv.Build G inv.
HB.instance Definition _ := Monoid_isGroup.Build G mulVg mulgV.
HB.end.
Bind Scope group_scope with Group.sort.
Section GroupTheory.
Variable G : groupType.
Implicit Types x y : G.
Lemma mulgV : right_inverse one inv (@mul G).
Definition divgg := mulgV.
Lemma mulKg : @left_loop G G (@inv G) *%g.
Lemma mulVKg : @rev_left_loop G G (@inv G) *%g.
Lemma mulgK : @right_loop G G (@inv G) *%g.
Lemma mulgVK : @rev_right_loop G G (@inv G) *%g.
Definition divgK := mulgVK.
Lemma mulgI : @right_injective G G G *%g.
Lemma mulIg : @left_injective G G G *%g.
Lemma divgI : @right_injective G G G (fun x y => x / y).
Lemma divIg : @left_injective G G G (fun x y => x / y).
Proof.
Lemma divg1 x : x / 1 = x
Lemma div1g x : 1 / x = x^-1
Proof.
Lemma divKg x y : commute x y -> x / (x / y) = y.
Lemma mulgKA z x y : (x * z) / (y * z) = x / y.
Lemma divgKA z x y : (x / z) * (z * y) = x * y.
Lemma mulg1_eq x y : x * y = 1 -> x^-1 = y.
Lemma divg1_eq x y : x / y = 1 -> x = y.
Lemma divg_eq x y z : (x / z == y) = (x == y * z).
Lemma divg_eq1 x y : (x / y == 1) = (x == y).
Lemma mulg_eq1 x y : (x * y == 1) = (x == y^-1).
Lemma commuteV x y : commute x y -> commute x y^-1.
Lemma expgnFr x m n : n <= m -> x ^+ (m - n) = x ^+ m / x ^+ n.
Lemma expgnFl x y n : commute x y -> (x / y) ^+ n = x ^+ n / y ^+ n.
Lemma conjgC x y : x * y = y * x ^ y.
Proof.
Lemma conjgCV x y : x * y = y ^ x^-1 * x.
Lemma conjg1 x : x ^ 1 = x.
Lemma conj1g x : 1 ^ x = 1.
Lemma conjMg x y z : (x * y) ^ z = x ^ z * y ^ z.
Lemma conjgM x y z : x ^ (y * z) = (x ^ y) ^ z.
Lemma conjVg x y : x^-1 ^ y = (x ^ y)^-1.
Lemma conjJg x y z : (x ^ y) ^ z = (x ^ z) ^ y ^ z.
Lemma conjXg x y n : (x ^+ n) ^ y = (x ^ y) ^+ n.
Lemma conjgK : @right_loop G G (@inv G) (@conjg G).
Lemma conjgKV : @rev_right_loop G G (@inv G) (@conjg G).
Lemma conjg_inj : @left_injective G G G (@conjg G).
Lemma conjg_eq1 x y : (x ^ y == 1) = (x == 1).
Lemma conjg_prod I r (P : pred I) (F : I -> G) z :
(\prod_(i <- r | P i) F i) ^ z = \prod_(i <- r | P i) (F i ^ z).
Lemma commgC x y : x * y = y * x * [~ x, y].
Lemma commgCV x y : x * y = [~ x^-1, y^-1] * (y * x).
Lemma conjRg x y z : [~ x, y] ^ z = [~ x ^ z, y ^ z].
Lemma invgR x y : [~ x, y]^-1 = [~ y, x].
Lemma commgP x y : reflect (commute x y) ([~ x, y] == 1).
Lemma conjg_fix x y : (x ^ y == x) = ([~ x, y] == 1).
Lemma conjg_fixP x y : reflect (x ^ y = x) ([~ x, y] == 1).
Lemma commg1_sym x y : ([~ x, y] == 1) = ([~ y, x] == 1).
Lemma commg1 x : [~ x, 1] = 1.
Lemma comm1g x : [~ 1, x] = 1.
Lemma commgg x : [~ x, x] = 1.
Lemma commgXg x n : [~ x, x ^+ n] = 1.
Lemma commgVg x : [~ x, x^-1] = 1.
Lemma commgXVg x n : [~ x, x ^- n] = 1.
Section ClosedPredicates.
Variable S : {pred G}.
Lemma group_closedV : group_closed S -> invg_closed S.
Proof.
Lemma group_closedM : group_closed S -> mulg_closed S.
Proof.
End ClosedPredicates.
End GroupTheory.
#[global] Hint Rewrite @mulg1 @mul1g invg1 @mulVg mulgV (@invgK) mulgK mulgVK
@invgM @mulgA : gsimpl.
Ltac gsimpl := autorewrite with gsimpl; try done.
Definition gsimp := (@mulg1, @mul1g, (@invg1, @invgK), (@mulgV, @mulVg)).
Definition gnorm := (gsimp, (@mulgK, @mulgVK, (@mulgA, @invgM))).
Arguments mulgI [G].
Arguments mulIg [G].
Arguments conjg_inj {G} x [x1 x2].
Arguments commgP {G x y}.
Arguments conjg_fixP {G x y}.
HB.mixin Record isMultiplicative (G H : magmaType) (apply : G -> H) := {
gmulfM : {morph apply : x y / x * y}
}.
HB.structure Definition Multiplicative (G H : magmaType) :=
{f of isMultiplicative G H f}.
HB.mixin Record Multiplicative_isUMagmaMorphism (G H : baseUMagmaType)
(f : G -> H) := {
gmulf1 : f 1 = 1
}.
HB.structure Definition UMagmaMorphism (G H : baseUMagmaType) :=
{f of Multiplicative_isUMagmaMorphism G H f & isMultiplicative G H f}.
Definition monoid_morphism (G H : baseUMagmaType) (f : G -> H) : Prop :=
(f 1 = 1) * {morph f : x y / x * y}.
HB.factory Record isUMagmaMorphism (G H : baseUMagmaType) (f : G -> H) := {
monoid_morphism_subproof : monoid_morphism f
}.
HB.builders Context G H apply & isUMagmaMorphism G H apply.
HB.instance Definition _ :=
isMultiplicative.Build G H apply monoid_morphism_subproof.2.
HB.instance Definition _ :=
Multiplicative_isUMagmaMorphism.Build G H apply monoid_morphism_subproof.1.
HB.end.
HB.factory Record isGroupMorphism (G H : groupType) (f : G -> H) := {
gmulfF : {morph f : x y / x / y}
}.
HB.builders Context G H apply & isGroupMorphism G H apply.
Local Lemma gmulf1 : apply 1 = 1.
Local Lemma gmulfM : {morph apply : x y / x * y}.
Proof.
HB.instance Definition _ := isMultiplicative.Build G H apply gmulfM.
HB.instance Definition _ :=
Multiplicative_isUMagmaMorphism.Build G H apply gmulf1.
HB.end.
Module MultiplicativeExports.
Notation "{ 'multiplicative' U -> V }" :=
(Multiplicative.type U%type V%type) : type_scope.
End MultiplicativeExports.
HB.export MultiplicativeExports.
#[non_forgetful_inheritance]
HB.instance Definition _ G H (f : UMagmaMorphism.type G H) :=
UMagmaMorphism.on (Multiplicative.sort f).
Section LiftedMagma.
Variables (T : Type) (G : magmaType).
Definition mul_fun (f g : T -> G) x := f x * g x.
End LiftedMagma.
Section LiftedBaseUMagma.
Variables (T : Type) (G : baseUMagmaType).
Definition one_fun : T -> G := fun=> 1.
End LiftedBaseUMagma.
Local Notation "\1" := (one_fun _) : function_scope.
Local Notation "f \* g" := (mul_fun f g) : function_scope.
Arguments one_fun {_} G _ /.
Arguments mul_fun {_ _} f g _ /.
Section MorphismTheory.
Section Magma.
Variables (G H : magmaType) (f : {multiplicative G -> H}).
Lemma can2_gmulfM f' : cancel f f' -> cancel f' f -> {morph f' : x y / x * y}.
Lemma gmulf_commute x y : commute x y -> commute (f x) (f y).
End Magma.
Section UMagma.
Variables (G H : umagmaType) (f : UMagmaMorphism.type G H).
Lemma gmulf_eq1 x : injective f -> (f x == 1) = (x == 1).
Lemma can2_gmulf1 f' : cancel f f' -> cancel f' f -> f' 1 = 1.
Lemma gmulfXn n : {morph f : x / x ^+ n}.
Lemma gmulf_prod I r (P : pred I) E :
f (\prod_(i <- r | P i) E i) = \prod_(i <- r | P i) f (E i).
End UMagma.
Section Group.
Variables (G H : groupType) (f : UMagmaMorphism.type G H).
Lemma gmulfV : {morph f : x / x^-1}.
Lemma gmulfF : {morph f : x y / x / y}.
Lemma gmulf_inj : (forall x, f x = 1 -> x = 1) -> injective f.
Lemma gmulfXVn n : {morph f : x / x ^- n}.
Lemma gmulfJ : {morph f : x y / x ^ y}.
Lemma gmulfR : {morph f : x y / [~ x, y]}.
End Group.
Section MulFun.
Variables (G H K : magmaType).
Variables (f g : {multiplicative H -> K}) (h : {multiplicative G -> H}).
Fact idfun_gmulfM : {morph @idfun G : x y / x * y}.
Proof.
by []. Qed.
Fact comp_gmulfM : {morph f \o h : x y / x * y}.
Proof.
End MulFun.
Section Mul1Fun.
Variables (G : magmaType) (H : umagmaType).
Fact idfun_gmulf1 : idfun 1 = 1 :> H.
Proof.
by []. Qed.
Multiplicative_isUMagmaMorphism.Build H H idfun idfun_gmulf1.
Fact one_fun_gmulfM : {morph @one_fun G H : x y / x * y}.
Proof.
isMultiplicative.Build G H (@one_fun G H) one_fun_gmulfM.
End Mul1Fun.
Section Mul11Fun.
Variables (G H K : umagmaType).
Variables (f g : UMagmaMorphism.type H K) (h : UMagmaMorphism.type G H).
Fact comp_gmulf1 : (f \o h) 1 = 1.
Proof.
HB.instance Definition _ :=
Multiplicative_isUMagmaMorphism.Build G K (f \o h) comp_gmulf1.
Fact one_fun_gmulf1 : @one_fun G H 1 = 1.
Proof.
by []. Qed.
Multiplicative_isUMagmaMorphism.Build G H (@one_fun G H) one_fun_gmulf1.
Fact mul_fun_gmulf1 : (f \* g) 1 = 1.
End Mul11Fun.
End MorphismTheory.
HB.mixin Record isMulClosed (G : magmaType) (S : {pred G}) := {
gpredM : mulg_closed S
}.
HB.mixin Record isMul1Closed (G : baseUMagmaType) (S : {pred G}) := {
gpred1 : 1 \in S
}.
HB.mixin Record isInvClosed (G : groupType) (S : {pred G}) := {
gpredVr : invg_closed S
}.
#[short(type="mulgClosed")]
HB.structure Definition MulClosed G := {S of isMulClosed G S}.
#[short(type="umagmaClosed")]
HB.structure Definition UMagmaClosed G :=
{S of isMul1Closed G S & isMulClosed G S}.
#[short(type="invgClosed")]
HB.structure Definition InvClosed G := {S of isInvClosed G S}.
#[short(type="groupClosed")]
HB.structure Definition GroupClosed G :=
{S of isInvClosed G S & isMul1Closed G S & isMulClosed G S}.
Section UMagmaPred.
Variables (G : baseUMagmaType).
Section UMagma.
Variables S : umagmaClosed G.
Lemma gpred_prod I r (P : pred I) F :
(forall i, P i -> F i \in S) -> \prod_(i <- r | P i) F i \in S.
Lemma gpredXn n : {in S, forall u, u ^+ n \in S}.
End UMagma.
End UMagmaPred.
Section GroupPred.
Variables (G : groupType).
Lemma gpredV (S : invgClosed G) : {mono (@inv G): u / u \in S}.
Section Group.
Variables S : groupClosed G.
Lemma gpredF : {in S &, forall u v, u / v \in S}.
Lemma gpredFC u v : (u / v \in S) = (v / u \in S).
Lemma gpredXNn n: {in S, forall u, u ^- n \in S}.
Lemma gpredMr x y : x \in S -> (y * x \in S) = (y \in S).
Lemma gpredMl x y : x \in S -> (x * y \in S) = (y \in S).
Proof.
Lemma gpredFr x y : x \in S -> (y / x \in S) = (y \in S).
Lemma gpredFl x y : x \in S -> (x / y \in S) = (y \in S).
Lemma gpredJ x y : x \in S -> y \in S -> x ^ y \in S.
Lemma gpredR x y : x \in S -> y \in S -> [~ x, y] \in S.
End Group.
End GroupPred.
HB.mixin Record isSubMagma (G : magmaType) (S : pred G) H
& SubType G S H & Magma H := {
valM_subproof : {morph (val : H -> G) : x y / x * y}
}.
#[short(type="subMagmaType")]
HB.structure Definition SubMagma (G : magmaType) S :=
{ H of SubChoice G S H & Magma H & isSubMagma G S H }.
Section subMagma.
Context (G : magmaType) (S : pred G) (H : subMagmaType S).
Notation val := (val : H -> G).
HB.instance Definition _ := isMultiplicative.Build H G val valM_subproof.
Lemma valM : {morph val : x y / x * y}
Proof.
HB.factory Record SubChoice_isSubMagma (G : magmaType) S H
& SubChoice G S H := {
mulg_closed_subproof : mulg_closed S
}.
HB.builders Context G S H & SubChoice_isSubMagma G S H.
HB.instance Definition _ := isMulClosed.Build G S mulg_closed_subproof.
Let inH v Sv : H := Sub v Sv.
Let mulH (u1 u2 : H) := inH (gpredM _ _ (valP u1) (valP u2)).
HB.instance Definition _ := hasMul.Build H mulH.
Lemma valM : {morph (val : H -> G) : x y / x * y}.
Proof.
HB.instance Definition _ := isSubMagma.Build G S H valM.
HB.end.
#[short(type="subSemigroupType")]
HB.structure Definition SubSemigroup (G : semigroupType) S :=
{ H of SubMagma G S H & Semigroup H}.
HB.factory Record SubChoice_isSubSemigroup (G : semigroupType) S H
& SubChoice G S H := {
mulg_closed_subproof : mulg_closed S
}.
HB.builders Context G S H & SubChoice_isSubSemigroup G S H.
HB.instance Definition _ :=
SubChoice_isSubMagma.Build G S H mulg_closed_subproof.
Lemma mulgA : associative (@mul H).
HB.instance Definition _ := isSemigroup.Build H mulgA.
HB.end.
HB.mixin Record isSubBaseUMagma (G : baseUMagmaType) (S : pred G) H
& SubMagma G S H & BaseUMagma H := {
val1_subproof : (val : H -> G) 1 = 1
}.
#[short(type="subBaseUMagmaType")]
HB.structure Definition SubBaseUMagma (G : umagmaType) S :=
{ H of SubMagma G S H & BaseUMagma H & isSubBaseUMagma G S H}.
#[short(type="subUMagmaType")]
HB.structure Definition SubUMagma (G : umagmaType) S :=
{ H of SubMagma G S H & UMagma H & isSubBaseUMagma G S H}.
Section subUMagma.
Context (G : umagmaType) (S : pred G) (H : subUMagmaType S).
Notation val := (val : H -> G).
HB.instance Definition _ :=
Multiplicative_isUMagmaMorphism.Build H G val val1_subproof.
Lemma val1 : val 1 = 1
Proof.
HB.factory Record SubChoice_isSubUMagma (G : umagmaType) S H
& SubChoice G S H := {
umagma_closed_subproof : umagma_closed S
}.
HB.builders Context G S H & SubChoice_isSubUMagma G S H.
HB.instance Definition _ :=
SubChoice_isSubMagma.Build G S H (snd umagma_closed_subproof).
Let inH v Sv : H := Sub v Sv.
Let oneH := inH (fst umagma_closed_subproof).
HB.instance Definition _ := hasOne.Build H oneH.
Lemma val1 : (val : H -> G) 1 = 1.
Proof.
exact/SubK. Qed.
HB.instance Definition _ := isSubBaseUMagma.Build G S H val1.
Lemma mul1g : left_id 1 (@mul H).
Lemma mulg1 : right_id 1 (@mul H).
HB.instance Definition _ := BaseUMagma_isUMagma.Build H mul1g mulg1.
HB.end.
#[short(type="subMonoidType")]
HB.structure Definition SubMonoid (G : monoidType) S :=
{ H of SubUMagma G S H & Monoid H}.
HB.factory Record SubChoice_isSubMonoid (G : monoidType) S H
& SubChoice G S H := {
monoid_closed_subproof : monoid_closed S
}.
HB.builders Context G S H & SubChoice_isSubMonoid G S H.
HB.instance Definition _ :=
SubChoice_isSubUMagma.Build G S H monoid_closed_subproof.
HB.instance Definition _ :=
SubChoice_isSubSemigroup.Build G S H (snd monoid_closed_subproof).
HB.end.
#[short(type="subGroupType")]
HB.structure Definition SubGroup (G : groupType) S :=
{ H of SubUMagma G S H & Group H}.
HB.factory Record SubChoice_isSubGroup (G : groupType) S H
& SubChoice G S H := {
group_closed_subproof : group_closed S
}.
HB.builders Context G S H & SubChoice_isSubGroup G S H.
Lemma umagma_closed : umagma_closed S.
Proof.
HB.instance Definition _ :=
isInvClosed.Build G S (group_closedV group_closed_subproof).
Let inH v Sv : H := Sub v Sv.
Let invH (u : H) := inH (gpredVr _ (valP u)).
HB.instance Definition _ := hasInv.Build H invH.
Lemma mulVg : left_inverse 1%g invH *%g.
Lemma mulgV : right_inverse 1%g invH *%g.
HB.instance Definition _ := Monoid_isGroup.Build H mulVg mulgV.
HB.end.
Prenex Implicits mul inv natexp conjg commg.
Notation "*%g" := (@mul _) : function_scope.
Notation "x * y" := (mul x y) : group_scope.
Notation "1" := (@one _) : group_scope.
Notation "s `_ i" := (nth 1 s i) : group_scope.
Notation "\prod_ ( i <- r | P ) F" :=
(\big[*%g/1]_(i <- r | P%B) F%g) : group_scope.
Notation "\prod_ ( i <- r ) F" :=
(\big[*%g/1]_(i <- r) F%g) : group_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
(\big[*%g/1]_(m <= i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( m <= i < n ) F" :=
(\big[*%g/1]_(m <= i < n) F%g) : group_scope.
Notation "\prod_ ( i | P ) F" :=
(\big[*%g/1]_(i | P%B) F%g) : group_scope.
Notation "\prod_ i F" :=
(\big[*%g/1]_i F%g) : group_scope.
Notation "\prod_ ( i : t | P ) F" :=
(\big[*%g/1]_(i : t | P%B) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i : t ) F" :=
(\big[*%g/1]_(i : t) F%g) (only parsing) : group_scope.
Notation "\prod_ ( i < n | P ) F" :=
(\big[*%g/1]_(i < n | P%B) F%g) : group_scope.
Notation "\prod_ ( i < n ) F" :=
(\big[*%g/1]_(i < n) F%g) : group_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
(\big[*%g/1]_(i in A | P%B) F%g) : group_scope.
Notation "\prod_ ( i 'in' A ) F" :=
(\big[*%g/1]_(i in A) F%g) : group_scope.
Notation "x ^+ n" := (natexp x n) : group_scope.
Notation "x ^-1" := (inv x) : group_scope.
Notation "x / y" := (x * y^-1) : group_scope.
Notation "x ^- n" := ((x ^+ n)^-1) : group_scope.
Notation "x ^ y" := (conjg x y) : group_scope.
Notation "[ ~ x1 , x2 , .. , xn ]" := (commg .. (commg x1 x2) .. xn)
: group_scope.
Section FinFunMagma.
Variable (aT : finType) (rT : magmaType).
Implicit Types f g : {ffun aT -> rT}.
Definition ffun_mul f g := [ffun a => f a * g a].
HB.instance Definition _ := hasMul.Build {ffun aT -> rT} ffun_mul.
End FinFunMagma.
HB.instance Definition _ (aT : finType) (rT : ChoiceMagma.type) :=
Magma.on {ffun aT -> rT}.
Section FinFunSemigroup.
Variable (aT : finType) (rT : semigroupType).
Implicit Types f g : {ffun aT -> rT}.
Fact ffun_mulgA : associative (@ffun_mul aT rT).
HB.instance Definition _ := isSemigroup.Build {ffun aT -> rT} ffun_mulgA.
End FinFunSemigroup.
Section FinFunBaseUMagma.
Variable (aT : finType) (rT : baseUMagmaType).
Implicit Types f g : {ffun aT -> rT}.
Definition ffun_one := [ffun a : aT => (1 : rT)].
HB.instance Definition _ :=
hasOne.Build {ffun aT -> rT} ffun_one.
End FinFunBaseUMagma.
HB.instance Definition _ (aT : finType) (rT : ChoiceBaseUMagma.type) :=
BaseUMagma.on {ffun aT -> rT}.
Section FinFunUMagma.
Variable (aT : finType) (rT : umagmaType).
Implicit Types f g : {ffun aT -> rT}.
Fact ffun_mul1g : left_id (@ffun_one aT rT) *%g.
Fact ffun_mulg1 : right_id (@ffun_one aT rT) *%g.
HB.instance Definition _ :=
Magma_isUMagma.Build {ffun aT -> rT} ffun_mul1g ffun_mulg1.
End FinFunUMagma.
HB.instance Definition _ (aT : finType) (rT : monoidType) :=
UMagma.on {ffun aT -> rT}.
Section FinFunBaseGroup.
Variable (aT : finType) (rT : baseGroupType).
Implicit Types f g : {ffun aT -> rT}.
Definition ffun_inv f := [ffun a => (f a)^-1].
HB.instance Definition _ := hasInv.Build {ffun aT -> rT} ffun_inv.
End FinFunBaseGroup.
Section FinFunGroup.
Variable (aT : finType) (rT : groupType).
Implicit Types f g : {ffun aT -> rT}.
Fact ffun_mulVg :
left_inverse (@ffun_one aT rT) (@ffun_inv _ _) (@ffun_mul _ _).
Fact ffun_mulgV :
right_inverse (@ffun_one aT rT) (@ffun_inv _ _) (@ffun_mul _ _).
HB.instance Definition _ := Monoid_isGroup.Build {ffun aT -> rT}
ffun_mulVg ffun_mulgV.
End FinFunGroup.
Section PairMagma.
Variables G H : magmaType.
Definition mul_pair (x y : G * H) := (x.1 * y.1, x.2 * y.2).
HB.instance Definition _ := hasMul.Build (G * H)%type mul_pair.
Fact fst_is_multiplicative : {morph fst : x y / x * y}
Proof.
by []. Qed.
isMultiplicative.Build _ _ fst fst_is_multiplicative.
Fact snd_is_multiplicative : {morph snd : x y / x * y}
Proof.
by []. Qed.
isMultiplicative.Build _ _ snd snd_is_multiplicative.
End PairMagma.
Section PairSemigroup.
Variables G H : semigroupType.
Lemma pair_mulgA : associative (@mul (G * H)%type).
HB.instance Definition _ := Magma_isSemigroup.Build (G * H)%type pair_mulgA.
End PairSemigroup.
Section PairBaseUMagma.
Variables G H : baseUMagmaType.
Definition one_pair : G * H := (1, 1).
HB.instance Definition _ := hasOne.Build (G * H)%type one_pair.
Fact fst_is_umagma_morphism : fst (1 : G * H) = 1
Proof.
by []. Qed.
Multiplicative_isUMagmaMorphism.Build _ _ fst fst_is_umagma_morphism.
Fact snd_is_umagma_morphism : snd (1 : G * H) = 1
Proof.
by []. Qed.
Multiplicative_isUMagmaMorphism.Build _ _ snd snd_is_umagma_morphism.
End PairBaseUMagma.
Section PairUMagma.
Variables G H : umagmaType.
Lemma pair_mul1g : left_id (@one_pair G H) *%g.
Lemma pair_mulg1 : right_id (@one_pair G H) *%g.
HB.instance Definition _ :=
BaseUMagma_isUMagma.Build (G * H)%type pair_mul1g pair_mulg1.
End PairUMagma.
HB.instance Definition _ (G H : ChoiceMagma.type) := Magma.on (G * H)%type.
HB.instance Definition _ (G H : ChoiceBaseUMagma.type) :=
BaseUMagma.on (G * H)%type.
HB.instance Definition _ (G H : monoidType) := Semigroup.on (G * H)%type.
Section PairBaseGroup.
Variables G H : baseGroupType.
Definition inv_pair (u : G * H) := (u.1 ^-1, u.2 ^-1).
HB.instance Definition _ := hasInv.Build (G * H)%type inv_pair.
End PairBaseGroup.
Section PairGroup.
Variables G H : groupType.
Lemma pair_mulVg : left_inverse one (@inv_pair G H) mul.
Lemma pair_mulgV : right_inverse one (@inv_pair G H) mul.
HB.instance Definition _ :=
Monoid_isGroup.Build (G * H)%type pair_mulVg pair_mulgV.
End PairGroup.