Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core.Require Import Algebra.Groups.Group.Require Import Algebra.Groups.FreeGroup.Require Import Algebra.Groups.GroupCoeq.Require Import Spaces.Finite.Require Import WildCat.LocalOpen Scope mc_scope.LocalOpen Scope mc_mult_scope.(** In this file we develop presentations of groups. *)(** The data of a group presentation *)RecordGroupPresentation := {
(** We have a type of generators *)
gp_generators : Type ;
(** An indexing type for relators *)
gp_rel_index : Type ;
(** The relators are picked out amongst elements of the free group on the generators. *)
gp_relators : gp_rel_index -> FreeGroup gp_generators;
}.(** Note: A relator is a relation in the form of "w = 1", any relation "w = v" can become a relator "wv^-1 = 1" for words v and w. *)(** Given the data of a group presentation we can construct the group. This is sometimes called the presented group. *)
GroupPresentation -> Group
GroupPresentation -> Group
X, I: Type R: I -> FreeGroup X
Group
exact (GroupCoeq
(FreeGroup_rec I (FreeGroup X) R)
(FreeGroup_rec I (FreeGroup X) (funx => @group_unit (FreeGroup X)))).Defined.(** A group [G] has a presentation if there exists a group presentation whose presented group is isomorphic to [G]. *)ClassHasPresentation (G : Group) := {
presentation : GroupPresentation;
grp_iso_presentation : GroupIsomorphism (group_gp presentation) G;
}.Coercionpresentation : HasPresentation >-> GroupPresentation.(** Here are a few finiteness properties of group presentations. *)(** A group presentation is finitely generated if its generating set is finite. *)ClassFinitelyGeneratedPresentation (P : GroupPresentation)
:= finite_gp_generators : Finite (gp_generators P).(** A group presentation is finitely related if its relators indexing set is finite. *)ClassFinitelyRelatedPresentation (P : GroupPresentation)
:= finite_gp_relators : Finite (gp_rel_index P).(** A group presentation is a finite presentation if it is finitely generated and related. *)ClassFinitePresentation (P : GroupPresentation) := {
fp_generators : FinitelyGeneratedPresentation P;
fp_relators : FinitelyRelatedPresentation P;
}.(** These directly translate into properties of groups. *)(** A group is finitely generated if it has a finitely generated presentation. *)ClassIsFinitelyGenerated (G : Group) := {
fg_presentation : HasPresentation G;
fg_presentation_fg : FinitelyGeneratedPresentation fg_presentation;
}.(** A group is finitely related if it has a finitely related presentation. *)ClassIsFinitelyRelated (G : Group) := {
fr_presentation : HasPresentation G;
fr_presentation_fr : FinitelyRelatedPresentation fr_presentation;
}.ClassIsFinitelyPresented (G : Group) := {
fp_presentation : HasPresentation G;
fp_presentation_fp : FinitePresentation fp_presentation;
}.(** ** Fundamental theorem of presentations of groups *)(** A group homomorphism from a presented group is determined with how the underlying map acts on generators subject to the condition that relators are sent to the unit. *)
funext: Funext G: Group P: HasPresentation G H: Group
{f : gp_generators P -> H &
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~> GroupHomomorphism G H
funext: Funext G: Group P: HasPresentation G H: Group
{f : gp_generators P -> H &
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~> GroupHomomorphism G H
funext: Funext G: Group P: HasPresentation G H: Group
{f : gp_generators P -> H &
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~> (group_gp P $-> H)
funext: Funext G: Group P: HasPresentation G H: Group
{f : gp_generators P -> H &
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~>
{h : FreeGroup (gp_generators P) $-> H &
(funx : FreeGroup (gp_rel_index P) =>
h
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
h
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x))}
funext: Funext G: Group P: HasPresentation G H: Group
Type
funext: Funext G: Group P: HasPresentation G H: Group
?A <~> (FreeGroup (gp_generators P) $-> H)
funext: Funext G: Group P: HasPresentation G H: Group
{f : gp_generators P -> H &
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~>
{x : _ &
((funh : FreeGroup (gp_generators P) $-> H =>
(funx : FreeGroup (gp_rel_index P) =>
h
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
h
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x)))
o ?f) x}
funext: Funext G: Group P: HasPresentation G H: Group
{f : gp_generators P -> H &
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit} <~>
{x : _ &
((funh : FreeGroup (gp_generators P) $-> H =>
(funx : FreeGroup (gp_rel_index P) =>
h
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
x)) ==
(funx : FreeGroup (gp_rel_index P) =>
h
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x)))
o equiv_freegroup_rec H (gp_generators P)) x}
funext: Funext G: Group P: HasPresentation G H: Group
foralla : gp_generators P -> H,
(forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H a (gp_relators P r) =
group_unit) <~>
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) a
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) a
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H
(forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit) <~>
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H
(forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit) ->
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x)) ->
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H
(forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit) ->
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit
forallx : FreeGroup (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit
foralla : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
(FreeGroup.map2 (gp_rel_index P)),
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(tr a)) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) (tr a))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit
foralla : FreeGroup.Words (gp_rel_index P),
(funw : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
(FreeGroup.map2 (gp_rel_index P)) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(tr w)) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) (tr w)))
(Coeq.coeq a)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit
forallb : FreeGroup.Words (gp_rel_index P) *
(gp_rel_index P + gp_rel_index P) *
FreeGroup.Words (gp_rel_index P),
transport
(funw : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
(FreeGroup.map2 (gp_rel_index P)) =>
equiv_freegroup_rec H
(gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P)
(tr w)) =
equiv_freegroup_rec H
(gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr w))) (Coeq.cglue b)
(?coeq' (FreeGroup.map1 (gp_rel_index P) b)) =
?coeq' (FreeGroup.map2 (gp_rel_index P) b)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit
foralla : FreeGroup.Words (gp_rel_index P),
(funw : Coeq.Coeq (FreeGroup.map1 (gp_rel_index P))
(FreeGroup.map2 (gp_rel_index P)) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(tr w)) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) (tr w)))
(Coeq.coeq a)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit w: FreeGroup.Words (gp_rel_index P)
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(tr (Coeq.coeq Core.nil))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq Core.nil)))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq (Core.cons a w)))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq (Core.cons a w))))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(tr (Coeq.coeq (Core.cons a w)))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq (Core.cons a w))))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
Trunc_rec
(Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
(funb0 : FreeGroup.Words (gp_generators P) *
(gp_generators P + gp_generators P) *
FreeGroup.Words (gp_generators P) =>
words_rec_coh (gp_generators P) H f
(snd (fst b0)) (fst (fst b0)) (snd b0)))
(match a with
| inl a => gp_relators P a
| inr a => - gp_relators P a
end *
words_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) w) =
Trunc_rec
(Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
(funb0 : FreeGroup.Words (gp_generators P) *
(gp_generators P + gp_generators P) *
FreeGroup.Words (gp_generators P) =>
words_rec_coh (gp_generators P) H f
(snd (fst b0)) (fst (fst b0)) (snd b0)))
(match a with
| inl _ => monunit_freegroup_type (gp_generators P)
| inr _ =>
- monunit_freegroup_type (gp_generators P)
end *
words_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P =>
monunit_freegroup_type (gp_generators P)) w)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
Trunc_rec
(Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
(funb0 : FreeGroup.Words (gp_generators P) *
(gp_generators P + gp_generators P) *
FreeGroup.Words (gp_generators P) =>
words_rec_coh (gp_generators P) H f
(snd (fst b0)) (fst (fst b0)) (snd b0)))
(match a with
| inl a => gp_relators P a
| inr a => - gp_relators P a
end *
words_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) w) =
?Goal1
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
?Goal1 = ?Goal0
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
Trunc_rec
(Coeq.Coeq_rec H (words_rec (gp_generators P) H f)
(funb0 : FreeGroup.Words (gp_generators P) *
(gp_generators P + gp_generators P) *
FreeGroup.Words (gp_generators P) =>
words_rec_coh (gp_generators P) H f
(snd (fst b0)) (fst (fst b0))
(snd b0)))
(match a with
| inl _ => monunit_freegroup_type (gp_generators P)
| inr _ =>
- monunit_freegroup_type (gp_generators P)
end *
words_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P =>
monunit_freegroup_type (gp_generators P)) w) =
?Goal0
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
match a with
| inl a => gp_relators P a
| inr a => - gp_relators P a
end *
FreeGroup_rec (gp_generators P) H f
(words_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) w) =
FreeGroup_rec (gp_generators P) H f
match a with
| inl _ => monunit_freegroup_type (gp_generators P)
| inr _ =>
- monunit_freegroup_type (gp_generators P)
end *
FreeGroup_rec (gp_generators P) H f
(words_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P =>
monunit_freegroup_type (gp_generators P)) w)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit a: (gp_rel_index P + gp_rel_index P)%type w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
match a with
| inl a => gp_relators P a
| inr a => - gp_relators P a
end =
FreeGroup_rec (gp_generators P) H f
match a with
| inl _ => monunit_freegroup_type (gp_generators P)
| inr _ =>
- monunit_freegroup_type (gp_generators P)
end
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit g: gp_rel_index P w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f (gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
(monunit_freegroup_type (gp_generators P))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit g: gp_rel_index P w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
(- gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
(- monunit_freegroup_type (gp_generators P))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit g: gp_rel_index P w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f
(- gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
(- monunit_freegroup_type (gp_generators P))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f
(gp_relators P r) = group_unit g: gp_rel_index P w: Core.list (gp_rel_index P + gp_rel_index P) IHw: equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (tr (Coeq.coeq w))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(tr (Coeq.coeq w)))
FreeGroup_rec (gp_generators P) H f (gp_relators P g) =
FreeGroup_rec (gp_generators P) H f
(monunit_freegroup_type (gp_generators P))
refine (p _ @ (grp_homo_unit _)^).
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x)) ->
forallr : gp_rel_index P,
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: (funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) x)) ==
(funx : FreeGroup (gp_rel_index P) =>
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x)) r: gp_rel_index P
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallx : FreeGroup (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) x) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x) r: gp_rel_index P
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H p: forallx : FreeGroup (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) x) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit) x) r: gp_rel_index P p':= p o freegroup_eta: forallx : FreeGroup.Words (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (freegroup_eta x)) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(freegroup_eta x))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H r: gp_rel_index P p': forallx : FreeGroup.Words (gp_rel_index P),
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P) (freegroup_eta x)) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(freegroup_eta x))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H r: gp_rel_index P p': equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P)
(freegroup_eta
(FreeGroup.word_sing
(gp_rel_index P)
(inl r)))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(freegroup_eta
(FreeGroup.word_sing
(gp_rel_index P)
(inl r))))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
group_unit
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H r: gp_rel_index P p': equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(gp_relators P)
(freegroup_eta
(FreeGroup.word_sing
(gp_rel_index P)
(inl r)))) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P))
(fun_ : gp_rel_index P => group_unit)
(freegroup_eta
(FreeGroup.word_sing
(gp_rel_index P)
(inl r))))
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(freegroup_eta
(FreeGroup.word_sing (gp_rel_index P) (inl r))))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H r: gp_rel_index P
FreeGroup_rec (gp_generators P) H f (gp_relators P r) =
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(freegroup_eta
(FreeGroup.word_sing (gp_rel_index P) (inl r))))
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H r: gp_rel_index P
equiv_freegroup_rec H (gp_generators P) f
(FreeGroup_rec (gp_rel_index P)
(FreeGroup (gp_generators P)) (gp_relators P)
(freegroup_eta
(FreeGroup.word_sing (gp_rel_index P) (inl r)))) =
FreeGroup_rec (gp_generators P) H f (gp_relators P r)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H r: gp_rel_index P
equiv_freegroup_rec H (gp_generators P) f
(gp_relators P r) *
equiv_freegroup_rec H (gp_generators P) f mon_unit =
FreeGroup_rec (gp_generators P) H f (gp_relators P r)
funext: Funext G: Group P: HasPresentation G H: Group f: gp_generators P -> H r: gp_rel_index P
equiv_freegroup_rec H (gp_generators P) f
(gp_relators P r) *
equiv_freegroup_rec H (gp_generators P) f mon_unit =
FreeGroup_rec (gp_generators P) H f (gp_relators P r) *
mon_unit
f_ap.Defined.(** ** Constructors for finite presentations *)
n, m: nat f: FinSeq m (FreeGroup (Fin n))
GroupPresentation
n, m: nat f: FinSeq m (FreeGroup (Fin n))
GroupPresentation
n, m: nat f: FinSeq m (FreeGroup (Fin n))
Type
n, m: nat f: FinSeq m (FreeGroup (Fin n))
Type
n, m: nat f: FinSeq m (FreeGroup (Fin n))
?gp_rel_index -> FreeGroup ?gp_generators
n, m: nat f: FinSeq m (FreeGroup (Fin n))
Type
exact (Fin n).
n, m: nat f: FinSeq m (FreeGroup (Fin n))
Type
exact (Fin m).
n, m: nat f: FinSeq m (FreeGroup (Fin n))
Fin m -> FreeGroup (Fin n)
exact f.Defined.
n, m: nat f: FinSeq m (FreeGroup (Fin n))
FinitelyGeneratedPresentation
(Build_Finite_GroupPresentation n m f)
n, m: nat f: FinSeq m (FreeGroup (Fin n))
FinitelyGeneratedPresentation
(Build_Finite_GroupPresentation n m f)
n, m: nat f: FinSeq m (FreeGroup (Fin n))
nat
n, m: nat f: FinSeq m (FreeGroup (Fin n))
merely
(gp_generators
(Build_Finite_GroupPresentation n m f) <~>
Fin ?fcard)
2: simpl; apply tr; reflexivity.Defined.
n, m: nat f: FinSeq m (FreeGroup (Fin n))
FinitelyRelatedPresentation
(Build_Finite_GroupPresentation n m f)
n, m: nat f: FinSeq m (FreeGroup (Fin n))
FinitelyRelatedPresentation
(Build_Finite_GroupPresentation n m f)
n, m: nat f: FinSeq m (FreeGroup (Fin n))
nat
n, m: nat f: FinSeq m (FreeGroup (Fin n))
merely
(gp_rel_index (Build_Finite_GroupPresentation n m f) <~>
Fin ?fcard)
2: simpl; apply tr; reflexivity.Defined.(** ** Notations for presentations *)(** Convenient abbreviation when defining notations. *)Local Notationff := (freegroup_in o fin_nat).(** TODO: I haven't worked out how to generalize to any number of binders, so we explicitly list the first few levels. *)LocalOpen Scope nat_scope.(** One generator *)Notation"⟨ x | F , .. , G ⟩" :=
(Build_Finite_GroupPresentation 1 _
(fscons ((fun (x : FreeGroup (Fin 1))
=> F : FreeGroup (Fin _)) (ff 0%nat))
.. (fscons ((fun (x : FreeGroup (Fin 1))
=> G : FreeGroup (Fin _)) (ff 0)) fsnil) ..))
(at level200, x binder).(** Two generators *)Notation"⟨ x , y | F , .. , G ⟩" :=
(Build_Finite_GroupPresentation 2 _
(fscons ((fun (xy : FreeGroup (Fin 2))
=> F : FreeGroup (Fin _)) (ff 0) (ff 1))
.. (fscons ((fun (xy : FreeGroup (Fin 2))
=> G : FreeGroup (Fin _)) (ff 0) (ff 1)) fsnil) ..))
(at level200, x binder, y binder).(** Three generators *)Notation"⟨ x , y , z | F , .. , G ⟩" :=
(Build_Finite_GroupPresentation 3 _
(fscons ((fun (xyz : FreeGroup (Fin 3))
=> F : FreeGroup (Fin _)) (ff 0) (ff 1) (ff 2))
.. (fscons ((fun (xyz : FreeGroup (Fin 3))
=> G : FreeGroup (Fin _)) (ff 0) (ff 1) (ff 2)) fsnil) ..))
(at level200, x binder, y binder, z binder).