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 PathAny.Require Import (notations) Classes.interfaces.canonical_names.Require Export (hints) Classes.interfaces.abstract_algebra.Require Export (hints) Classes.interfaces.canonical_names.(** We only export the parts of these that will be most useful to users of this file. *)Require Export Classes.interfaces.canonical_names (SgOp, sg_op, One, one,
MonUnit, mon_unit, LeftIdentity, left_identity, RightIdentity, right_identity,
Negate, negate, Associative, simple_associativity, associativity,
LeftInverse, left_inverse, RightInverse, right_inverse, Commutative, commutativity).Export canonical_names.BinOpNotations.Require Export Classes.interfaces.abstract_algebra (IsGroup(..), group_monoid, negate_l, negate_r,
IsSemiGroup(..), sg_set, sg_ass,
IsMonoid(..), monoid_left_id, monoid_right_id, monoid_semigroup,
IsMonoidPreserving(..), monmor_unitmor, monmor_sgmor,
IsSemiGroupPreserving, preserves_sg_op, IsUnitPreserving, preserves_mon_unit).Require Export Classes.theory.groups.Require Import Pointed.Core.Require Import WildCat.Require Import Spaces.Nat.Core.Require Import Truncations.Core.Local Set Polymorphic Inductive Cumulativity.Generalizable VariablesG H A B C f g.Declare Scope group_scope.(** * Groups *)(** A group is an abstraction of several common situations in mathematics. For example, consider the symmetries of an object. Two symmetries can be combined; there is a symmetry that does nothing; and any symmetry can be reversed. Such situations arise in geometry, algebra and, importantly for us, homotopy theory. *)LocalOpen Scope pointed_scope.LocalOpen Scope mc_mult_scope.LocalOpen Scope wc_iso_scope.(** ** Definition of a Group *)(** A group consists of a type, an operation on that type, a unit and an inverse that satisfy the group axioms in [IsGroup]. *)RecordGroup := {
group_type :> Type;
group_sgop :: SgOp group_type;
group_unit :: MonUnit group_type;
group_inverse :: Negate group_type;
group_isgroup :: IsGroup group_type;
}.Arguments group_sgop {_}.Arguments group_unit {_}.Arguments group_inverse {_}.Arguments group_isgroup {_}.(** We should never need to unfold the proof that something is a group. *)GlobalOpaque group_isgroup.Definitionissig_group : _ <~> Group
:= ltac:(issig).(** ** Proof automation *)(** Many times in group theoretic proofs we want some form of automation for obvious identities. Here we implement such a behavior. *)(** We create a database of hints for the group theory library *)Create HintDb group_db.(** Our group laws can be proven easily with tactics such as [rapply associativity]. However this requires a typeclass search on more general algebraic structures. Therefore we explicitly list many groups laws here so that coq can use them. We also create hints for each law in our groups database. *)SectionGroupLaws.Context {G : Group} (xyz : G).Definitiongrp_assoc := associativity x y z.Definitiongrp_unit_l := left_identity x.Definitiongrp_unit_r := right_identity x.Definitiongrp_inv_l := left_inverse x.Definitiongrp_inv_r := right_inverse x.EndGroupLaws.#[export] Hint Immediate grp_assoc : group_db.#[export] Hint Immediate grp_unit_l : group_db.#[export] Hint Immediate grp_unit_r : group_db.#[export] Hint Immediate grp_inv_l : group_db.#[export] Hint Immediate grp_inv_r : group_db.(** Given path types in a product we may want to decompose. *)#[export] Hint Extern5 (@paths (_ * _) _ _) => (apply path_prod) : group_db.(** Given path types in a sigma type of a hprop family (i.e. a subset) we may want to decompose. *)#[export] Hint Extern6 (@paths (sig _) _ _) => (rapply path_sigma_hprop) : group_db.(** We also declare a tactic (notation) for automatically solving group laws *)(** TODO: improve this tactic so that it also rewrites and is able to solve basic group lemmas. *)Tactic Notation"grp_auto" := hnf; intros; eauto with group_db.(** * Some basic properties of groups *)(** Groups are pointed sets with point the identity. *)Global Instanceispointed_group (G : Group)
: IsPointed G := @mon_unit G _.Definitionptype_group : Group -> pType
:= funG => [G, _].Coercionptype_group : Group >-> pType.(** An element acting like the identity is unique. *)Definitionidentity_unique {A : Type} {Aop : SgOp A}
(xy : A) {p : LeftIdentity Aop x} {q : RightIdentity Aop y}
: x = y := (q x)^ @ p y.Definitionidentity_unique' {A : Type} {Aop : SgOp A}
(xy : A) {p : LeftIdentity Aop x} {q : RightIdentity Aop y}
: y = x := (identity_unique x y)^.(** An element acting like an inverse is unique. *)
A: Type Aop: SgOp A Aunit: MonUnit A H: IsMonoid A a, x, y: A p: x * a = mon_unit q: a * y = mon_unit
x = y
A: Type Aop: SgOp A Aunit: MonUnit A H: IsMonoid A a, x, y: A p: x * a = mon_unit q: a * y = mon_unit
x = y
A: Type Aop: SgOp A Aunit: MonUnit A H: IsMonoid A a, x, y: A p: x * a = mon_unit q: a * y = mon_unit
x * (a * y) = y
A: Type Aop: SgOp A Aunit: MonUnit A H: IsMonoid A a, x, y: A p: x * a = mon_unit q: a * y = mon_unit
x * a * y = y
A: Type Aop: SgOp A Aunit: MonUnit A H: IsMonoid A a, x, y: A p: x * a = mon_unit q: a * y = mon_unit
mon_unit * y = y
apply left_identity.Defined.(** ** Group homomorphisms *)(** Group homomorphisms are maps between groups that preserve the group operation. They allow us to compare groups and map their structure to one another. This is useful for determining if two groups are really the same, in which case we say they are "isomorphic". *)(** A group homomorphism consists of a map between groups and a proof that the map preserves the group operation. *)RecordGroupHomomorphism (GH : Group) := Build_GroupHomomorphism' {
grp_homo_map :> group_type G -> group_type H;
grp_homo_ishomo :: IsMonoidPreserving grp_homo_map;
}.(** Group homomorphisms are pointed maps. *)Definitionpmap_GroupHomomorphism {GH : Group} (f : GroupHomomorphism G H) : G ->* H
:= Build_pMap G H f (@monmor_unitmor _ _ _ _ _ _ _ (@grp_homo_ishomo G H f)).Coercionpmap_GroupHomomorphism : GroupHomomorphism >-> pForall.Definitionissig_GroupHomomorphism (GH : Group) : _ <~> GroupHomomorphism G H
:= ltac:(issig).(** Function extensionality for group homomorphisms. *)
F: Funext G, H: Group g, h: GroupHomomorphism G H
g == h <~> g = h
F: Funext G, H: Group g, h: GroupHomomorphism G H
g == h <~> g = h
F: Funext G, H: Group g, h: GroupHomomorphism G H
g == h <~>
(issig_GroupHomomorphism G H)^-1 g =
(issig_GroupHomomorphism G H)^-1 h
F: Funext G, H: Group g, h: GroupHomomorphism G H
g == h <~>
((issig_GroupHomomorphism G H)^-1 g).1 =
((issig_GroupHomomorphism G H)^-1 h).1
apply equiv_path_forall.Defined.(** Group homomorphisms are sets, in the presence of funext. *)
F: Funext G, H: Group
IsHSet (GroupHomomorphism G H)
F: Funext G, H: Group
IsHSet (GroupHomomorphism G H)
F: Funext G, H: Group
is_mere_relation (GroupHomomorphism G H) paths
intros f g; apply (istrunc_equiv_istrunc _ equiv_path_grouphomomorphism).Defined.(** ** Basic properties of group homomorphisms *)(** Group homomorphisms preserve identities. *)
G, H: Group f: GroupHomomorphism G H
f mon_unit = mon_unit
G, H: Group f: GroupHomomorphism G H
f mon_unit = mon_unit
apply monmor_unitmor.Defined.#[export] Hint Immediate grp_homo_unit : group_db.(** Group homomorphisms preserve group operations. *)
G, H: Group f: GroupHomomorphism G H
forallxy : G, f (x * y) = f x * f y
G, H: Group f: GroupHomomorphism G H
forallxy : G, f (x * y) = f x * f y
apply monmor_sgmor.Defined.#[export] Hint Immediate grp_homo_op : group_db.(** Group homomorphisms preserve inverses. *)
G, H: Group f: GroupHomomorphism G H
forallx : G, f (- x) = - f x
G, H: Group f: GroupHomomorphism G H
forallx : G, f (- x) = - f x
G, H: Group f: GroupHomomorphism G H x: G
f (- x) = - f x
G, H: Group f: GroupHomomorphism G H x: G
f (- x) * f x = mon_unit
G, H: Group f: GroupHomomorphism G H x: G
f x * - f x = mon_unit
G, H: Group f: GroupHomomorphism G H x: G
f (- x) * f x = mon_unit
G, H: Group f: GroupHomomorphism G H x: G
f (- x) * f x = f mon_unit
G, H: Group f: GroupHomomorphism G H x: G
f (- x * x) = f mon_unit
G, H: Group f: GroupHomomorphism G H x: G
- x * x = mon_unit
apply grp_inv_l.
G, H: Group f: GroupHomomorphism G H x: G
f x * - f x = mon_unit
apply grp_inv_r.Defined.#[export] Hint Immediate grp_homo_inv : group_db.(** When building a group homomorphism we only need that it preserves the group operation, since we can prove that the identity is preserved. *)
G, H: Group f: G -> H h: IsSemiGroupPreserving f
GroupHomomorphism G H
G, H: Group f: G -> H h: IsSemiGroupPreserving f
GroupHomomorphism G H
G, H: Group f: G -> H h: IsSemiGroupPreserving f
IsMonoidPreserving f
G, H: Group f: G -> H h: IsSemiGroupPreserving f
IsSemiGroupPreserving f
G, H: Group f: G -> H h: IsSemiGroupPreserving f
IsUnitPreserving f
G, H: Group f: G -> H h: IsSemiGroupPreserving f
IsUnitPreserving f
G, H: Group f: G -> H h: IsSemiGroupPreserving f
f mon_unit = mon_unit
G, H: Group f: G -> H h: IsSemiGroupPreserving f
f mon_unit * f mon_unit = f mon_unit * mon_unit
G, H: Group f: G -> H h: IsSemiGroupPreserving f
f mon_unit * f mon_unit = f mon_unit
G, H: Group f: G -> H h: IsSemiGroupPreserving f
f mon_unit * f mon_unit = f (mon_unit * mon_unit)
G, H: Group f: G -> H h: IsSemiGroupPreserving f
f (mon_unit * mon_unit) = f mon_unit * f mon_unit
apply h.Defined.(** The identity map is a group homomorphism. *)Definitiongrp_homo_id {G : Group} : GroupHomomorphism G G
:= Build_GroupHomomorphism idmap.(** The composition of the underlying functions of two group homomorphisms is also a group homomorphism. *)
G, H, K: Group
GroupHomomorphism H K ->
GroupHomomorphism G H -> GroupHomomorphism G K
G, H, K: Group
GroupHomomorphism H K ->
GroupHomomorphism G H -> GroupHomomorphism G K
G, H, K: Group f: GroupHomomorphism H K g: GroupHomomorphism G H
GroupHomomorphism G K
srapply (Build_GroupHomomorphism (f o g)).Defined.(** ** Group Isomorphisms *)(** Group isomorphsims are group homomorphisms whose underlying map happens to be an equivalence. They allow us to consider two groups to be the "same". They can be inverted and composed just like equivalences. *)(** An isomorphism of groups is defined as group homomorphism that is an equivalence. *)RecordGroupIsomorphism (GH : Group) := Build_GroupIsomorphism {
grp_iso_homo :> GroupHomomorphism G H;
isequiv_group_iso :: IsEquiv grp_iso_homo;
}.(** We can build an isomorphism from an operation-preserving equivalence. *)
G, H: Group f: G <~> H h: IsSemiGroupPreserving f
GroupIsomorphism G H
G, H: Group f: G <~> H h: IsSemiGroupPreserving f
GroupIsomorphism G H
G, H: Group f: G <~> H h: IsSemiGroupPreserving f
GroupHomomorphism G H
G, H: Group f: G <~> H h: IsSemiGroupPreserving f
IsEquiv ?grp_iso_homo
G, H: Group f: G <~> H h: IsSemiGroupPreserving f
IsEquiv (Build_GroupHomomorphism f)
exact _.Defined.Definitionissig_GroupIsomorphism (GH : Group)
: _ <~> GroupIsomorphism G H := ltac:(issig).(** The underlying equivalence of a group isomorphism. *)Definitionequiv_groupisomorphism {GH : Group}
: GroupIsomorphism G H -> G <~> H
:= funf => Build_Equiv G H f _.Coercionequiv_groupisomorphism : GroupIsomorphism >-> Equiv.(** The underlying pointed equivalence of a group isomorphism. *)Definitionpequiv_groupisomorphism {AB : Group}
: GroupIsomorphism A B -> (A <~>* B)
:= funf => Build_pEquiv _ _ f _.Coercionpequiv_groupisomorphism : GroupIsomorphism >-> pEquiv.(** Funext for group isomorphisms. *)
F: Funext G, H: Group f, g: GroupIsomorphism G H
f == g <~> f = g
F: Funext G, H: Group f, g: GroupIsomorphism G H
f == g <~> f = g
F: Funext G, H: Group f, g: GroupIsomorphism G H
f == g <~>
(issig_GroupIsomorphism G H)^-1 f =
(issig_GroupIsomorphism G H)^-1 g
F: Funext G, H: Group f, g: GroupIsomorphism G H
f == g <~>
((issig_GroupIsomorphism G H)^-1 f).1 =
((issig_GroupIsomorphism G H)^-1 g).1
apply equiv_path_grouphomomorphism.Defined.(** Group isomorphisms form a set. *)
F: Funext G, H: Group
IsHSet (GroupIsomorphism G H)
F: Funext G, H: Group
IsHSet (GroupIsomorphism G H)
F: Funext G, H: Group
is_mere_relation (GroupIsomorphism G H) paths
intros f g; apply (istrunc_equiv_istrunc _ (equiv_path_groupisomorphism _ _)).Defined.(** The identity map is an equivalence and therefore a group isomorphism. *)Definitiongrp_iso_id {G : Group} : GroupIsomorphism G G
:= Build_GroupIsomorphism _ _ grp_homo_id _.(** Group isomorphisms can be composed by composing the underlying group homomorphism. *)Definitiongrp_iso_compose {GHK : Group}
(g : GroupIsomorphism H K) (f : GroupIsomorphism G H)
: GroupIsomorphism G K
:= Build_GroupIsomorphism _ _ (grp_homo_compose g f) _.(** Group isomorphisms can be inverted. The inverse map of the underlying equivalence also preserves the group operation and unit. *)
G, H: Group
GroupIsomorphism G H -> GroupIsomorphism H G
G, H: Group
GroupIsomorphism G H -> GroupIsomorphism H G
G, H: Group f: GroupHomomorphism G H e: IsEquiv f
GroupIsomorphism H G
G, H: Group f: GroupHomomorphism G H e: IsEquiv f
GroupHomomorphism H G
G, H: Group f: GroupHomomorphism G H e: IsEquiv f
IsEquiv ?grp_iso_homo
G, H: Group f: GroupHomomorphism G H e: IsEquiv f
GroupHomomorphism H G
srapply (Build_GroupHomomorphism f^-1).
G, H: Group f: GroupHomomorphism G H e: IsEquiv f
IsEquiv (Build_GroupHomomorphism f^-1)
exact _.Defined.(** Group isomorphism is a reflexive relation. *)Global Instancereflexive_groupisomorphism
: Reflexive GroupIsomorphism
:= funG => grp_iso_id.(** Group isomorphism is a symmetric relation. *)Global Instancesymmetric_groupisomorphism
: Symmetric GroupIsomorphism
:= funGH => grp_iso_inverse.(** Group isomorphism is a transitive relation. *)Global Instancetransitive_groupisomorphism
: Transitive GroupIsomorphism
:= funGHKfg => grp_iso_compose g f.(** Under univalence, equality of groups is equivalent to isomorphism of groups. This is the structure identity principle for groups. *)
U: Univalence G, H: Group
GroupIsomorphism G H <~> G = H
U: Univalence G, H: Group
GroupIsomorphism G H <~> G = H
U: Univalence G, H: Group
{f : G <~> H & IsMonoidPreserving f} <~> G = H
U: Univalence G, H: Group
GroupIsomorphism G H <~>
{f : G <~> H & IsMonoidPreserving f}
U: Univalence G, H: Group
{f : G <~> H & IsMonoidPreserving f} <~> G = H
U: Univalence
forallb : {H : Type &
{H0 : SgOp H &
{H1 : MonUnit H & {H2 : Negate H & IsGroup H}}}},
{f : issig_group b <~> issig_group b &
IsMonoidPreserving f}
U: Univalence
forallb1 : {H : Type &
{H0 : SgOp H &
{H1 : MonUnit H & {H2 : Negate H & IsGroup H}}}},
Contr
{b2
: {H : Type &
{H0 : SgOp H &
{H1 : MonUnit H & {H2 : Negate H & IsGroup H}}}} &
{f : issig_group b1 <~> issig_group b2 &
IsMonoidPreserving f}}
U: Univalence
forallb : {H : Type &
{H0 : SgOp H &
{H1 : MonUnit H & {H2 : Negate H & IsGroup H}}}},
{f : issig_group b <~> issig_group b &
IsMonoidPreserving f}
U: Univalence G: Type proj1: SgOp G proj0: MonUnit G proj2: Negate G proj3: IsGroup G
U: Univalence G: Type proj1: SgOp G proj0: MonUnit G proj2: Negate G proj3: IsGroup G
IsMonoidPreserving 1%equiv
exact _.
U: Univalence
forallb1 : {H : Type &
{H0 : SgOp H &
{H1 : MonUnit H & {H2 : Negate H & IsGroup H}}}},
Contr
{b2
: {H : Type &
{H0 : SgOp H &
{H1 : MonUnit H & {H2 : Negate H & IsGroup H}}}} &
{f : issig_group b1 <~> issig_group b2 &
IsMonoidPreserving f}}
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
Contr
{b2
: {H : Type &
{H0 : SgOp H &
{H1 : MonUnit H & {H2 : Negate H & IsGroup H}}}} &
{f : G <~> b2.1 & IsMonoidPreserving f}}
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
Contr
{y
: {H0 : SgOp G &
{H1 : MonUnit G & {H2 : Negate G & IsGroup G}}} &
IsMonoidPreserving 1%equiv}
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
IsGroup G
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
IsMonoidPreserving idmap
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
forally : {y
: {H0 : SgOp G &
{H1 : MonUnit G & {H2 : Negate G & IsGroup G}}}
& IsMonoidPreserving idmap},
((op; unit; neg; ?Goal0); ?Goal1) = y
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
IsMonoidPreserving idmap
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
forally : {y
: {H0 : SgOp G &
{H1 : MonUnit G & {H2 : Negate G & IsGroup G}}}
& IsMonoidPreserving idmap},
((op; unit; neg; ax); ?Goal0) = y
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G
forally : {y
: {H0 : SgOp G &
{H1 : MonUnit G & {H2 : Negate G & IsGroup G}}}
& IsMonoidPreserving idmap},
((op; unit; neg; ax); id_monoid_morphism) = y
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
(op; unit; neg; ax) = (op'; unit'; neg'; ax')
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
((op; unit; neg); ax) = ((op'; unit'; neg'); ax')
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
(op; unit; neg) = (op'; unit'; neg')
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
op = op'
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
transport
(fun_ : SgOp G => {_ : MonUnit G & Negate G})
?p (unit; neg) = (unit'; neg')
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
transport
(fun_ : SgOp G => {_ : MonUnit G & Negate G})
(path_forall op op'
((funx : G =>
path_forall (op x) (op' x)
((funy : G => letX := monmor_sgmor in X x y)
:
op x == op' x))
:
op == op')) (unit; neg) = (unit'; neg')
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
(unit; neg) = (unit'; neg')
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
unit = unit'
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
transport (fun_ : MonUnit G => Negate G) ?p neg =
neg'
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
transport (fun_ : MonUnit G => Negate G)
(letX := monmor_unitmor in X) neg = neg'
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap
neg = neg'
U: Univalence G: Type op: SgOp G unit: MonUnit G neg: Negate G ax: IsGroup G op': SgOp G unit': MonUnit G neg': Negate G ax': IsGroup G eq: IsMonoidPreserving idmap x: G
neg x = neg' x
exact (preserves_negate (f:=idmap) _).
U: Univalence G, H: Group
GroupIsomorphism G H <~>
{f : G <~> H & IsMonoidPreserving f}
make_equiv.Defined.(** A version with nicer universe variables. *)Definitionequiv_path_group@{u v | u < v} {U : Univalence} {G H : Group@{u}}
: GroupIsomorphism G H <~> (paths@{v} G H)
:= equiv_path_group'.(** ** Simple group equivalences *)(** Left multiplication is an equivalence. *)
G: Group
forallx : G, IsEquiv (sg_op x)
G: Group
forallx : G, IsEquiv (sg_op x)
G: Group x: G
IsEquiv (sg_op x)
G: Group x: G
G -> G
G: Group x: G
sg_op x o ?g == idmap
G: Group x: G
?g o sg_op x == idmap
G: Group x: G
sg_op x o sg_op (- x) == idmap
G: Group x: G
sg_op (- x) o sg_op x == idmap
G: Group x, y: G
x * (- x * y) = y
G: Group x, y: G
- x * (x * y) = y
G: Group x, y: G
x * - x * y = mon_unit * y
G: Group x, y: G
- x * x * y = mon_unit * y
G: Group x, y: G
x * - x = mon_unit
G: Group x, y: G
- x * x = mon_unit
G: Group x, y: G
- x * x = mon_unit
apply grp_inv_l.Defined.(** Right multiplication is an equivalence. *)
G: Group
forallx : G, IsEquiv (funy : G => y * x)
G: Group
forallx : G, IsEquiv (funy : G => y * x)
G: Group x: G
IsEquiv (funy : G => y * x)
G: Group x: G
G -> G
G: Group x: G
(funy : G => y * x) o ?g == idmap
G: Group x: G
?g o (funy : G => y * x) == idmap
G: Group x: G
(funy : G => y * x) o (funy : G => y * - x) == idmap
G: Group x: G
(funy : G => y * - x) o (funy : G => y * x) == idmap
G: Group x, y: G
y * - x * x = y
G: Group x, y: G
y * x * - x = y
G: Group x, y: G
y * (- x * x) = y * mon_unit
G: Group x, y: G
y * (x * - x) = y * mon_unit
G: Group x, y: G
- x * x = mon_unit
G: Group x, y: G
x * - x = mon_unit
G: Group x, y: G
x * - x = mon_unit
apply grp_inv_r.Defined.(** The operation inverting group elements is an equivalence. Note that, since the order of the operation will change after inversion, this isn't a group homomorphism. *)
G: Group
IsEquiv (negate : G -> G)
G: Group
IsEquiv (negate : G -> G)
G: Group
G -> G
G: Group
negate o ?g == idmap
G: Group
?g o negate == idmap
G: Group
negate o negate == idmap
G: Group
negate o negate == idmap
all: intro; apply negate_involutive.Defined.(** ** Reasoning with equations in groups. *)SectionGroupEquations.Context {G : Group} (xyz : G).(** Inverses are involutive. *)Definitiongrp_inv_inv : --x = x := negate_involutive x.(** Inverses distribute over the group operation. *)Definitiongrp_inv_op : - (x * y) = -y * -x := negate_sg_op x y.EndGroupEquations.(** ** Cancelation lemmas *)(** Group elements can be cancelled both on the left and the right. *)Definitiongrp_cancelL {G : Group} {xy : G} z : x = y <~> z * x = z * y
:= equiv_ap (funx => z * x) _ _.Definitiongrp_cancelR {G : Group} {xy : G} z : x = y <~> x * z = y * z
:= equiv_ap (funx => x * z) _ _.(** ** Group movement lemmas *)SectionGroupMovement.(** Since left/right multiplication is an equivalence, we can use lemmas about moving equivalences around to prove group movement lemmas. *)Context {G : Group} {xyz : G}.(** *** Moving group elements *)Definitiongrp_moveL_gM : x * -z = y <~> x = y * z
:= equiv_moveL_equiv_M (f := funt => t * z) _ _.Definitiongrp_moveL_Mg : -y * x = z <~> x = y * z
:= equiv_moveL_equiv_M (f := funt => y * t) _ _.Definitiongrp_moveR_gM : x = z * -y <~> x * y = z
:= equiv_moveR_equiv_M (f := funt => t * y) _ _.Definitiongrp_moveR_Mg : y = -x * z <~> x * y = z
:= equiv_moveR_equiv_M (f := funt => x * t) _ _.(** *** Moving inverses.*)(** These are the inverses of the previous but are included here for completeness*)Definitiongrp_moveR_gV : x = y * z <~> x * -z = y
:= equiv_moveR_equiv_V (f := funt => t * z) _ _.Definitiongrp_moveR_Vg : x = y * z <~> -y * x = z
:= equiv_moveR_equiv_V (f := funt => y * t) _ _.Definitiongrp_moveL_gV : x * y = z <~> x = z * -y
:= equiv_moveL_equiv_V (f := funt => t * y) _ _.Definitiongrp_moveL_Vg : x * y = z <~> y = -x * z
:= equiv_moveL_equiv_V (f := funt => x * t) _ _.(** We close the section here so the previous lemmas generalise their assumptions. *)EndGroupMovement.SectionGroupMovement.Context {G : Group} {xyz : G}.(** *** Moving elements equal to unit. *)Definitiongrp_moveL_1M : x * -y = mon_unit <~> x = y
:= equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gM.Definitiongrp_moveL_1V : x * y = mon_unit <~> x = -y
:= equiv_concat_r (grp_unit_l _) _ oE grp_moveL_gV.Definitiongrp_moveL_M1 : -y * x = mon_unit <~> x = y
:= equiv_concat_r (grp_unit_r _) _ oE grp_moveL_Mg.Definitiongrp_moveR_1M : mon_unit = y * (-x) <~> x = y
:= (equiv_concat_l (grp_unit_l _) _)^-1%equiv oE grp_moveR_gM.Definitiongrp_moveR_M1 : mon_unit = -x * y <~> x = y
:= (equiv_concat_l (grp_unit_r _) _)^-1%equiv oE grp_moveR_Mg.(** *** Cancelling elements equal to unit. *)Definitiongrp_cancelL1 : x = mon_unit <~> z * x = z
:= (equiv_concat_r (grp_unit_r _) _ oE grp_cancelL z).Definitiongrp_cancelR1 : x = mon_unit <~> x * z = z
:= (equiv_concat_r (grp_unit_l _) _) oE grp_cancelR z.EndGroupMovement.(** ** Power operation *)(** For a given [n : nat] we can define the [n]th power of a group element. *)Definitiongrp_pow {G : Group} (g : G) (n : nat) : G := nat_iter n (g *.) mon_unit.(** Any homomorphism respects [grp_pow]. *)
G, H: Group f: GroupHomomorphism G H n: nat g: G
f (grp_pow g n) = grp_pow (f g) n
G, H: Group f: GroupHomomorphism G H n: nat g: G
f (grp_pow g n) = grp_pow (f g) n
G, H: Group f: GroupHomomorphism G H g: G
f (grp_pow g 0) = grp_pow (f g) 0
G, H: Group f: GroupHomomorphism G H n: nat g: G IHn: f (grp_pow g n) = grp_pow (f g) n
f (grp_pow g n.+1) = grp_pow (f g) n.+1
G, H: Group f: GroupHomomorphism G H g: G
f (grp_pow g 0) = grp_pow (f g) 0
G, H: Group f: GroupHomomorphism G H g: G
f mon_unit = mon_unit
apply grp_homo_unit.
G, H: Group f: GroupHomomorphism G H n: nat g: G IHn: f (grp_pow g n) = grp_pow (f g) n
f (grp_pow g n.+1) = grp_pow (f g) n.+1
G, H: Group f: GroupHomomorphism G H n: nat g: G IHn: f (grp_pow g n) = grp_pow (f g) n
f (g * nat_iter n (sg_op g) mon_unit) =
f g * nat_iter n (sg_op (f g)) mon_unit
G, H: Group f: GroupHomomorphism G H n: nat g: G IHn: f (grp_pow g n) = grp_pow (f g) n
f g * f (grp_pow g n) =
f g * nat_iter n (sg_op (f g)) mon_unit
exact (ap (funm => f g + m) IHn).Defined.(** ** The category of Groups *)(** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *)Global Instanceisgraph_group : IsGraph Group
:= Build_IsGraph Group GroupHomomorphism.Global Instanceis01cat_group : Is01Cat Group :=
Build_Is01Cat Group _ (@grp_homo_id) (@grp_homo_compose).(** Helper notation so that the wildcat instances can easily be inferred. *)Local Notationgrp_homo_map' A B := (@grp_homo_map A B : _ -> (group_type A $-> _)).Global Instanceis2graph_group : Is2Graph Group
:= funAB => isgraph_induced (grp_homo_map' A B).Global Instanceisgraph_grouphomomorphism {AB : Group} : IsGraph (A $-> B)
:= isgraph_induced (grp_homo_map' A B).Global Instanceis01cat_grouphomomorphism {AB : Group} : Is01Cat (A $-> B)
:= is01cat_induced (grp_homo_map' A B).Global Instanceis0gpd_grouphomomorphism {AB : Group}: Is0Gpd (A $-> B)
:= is0gpd_induced (grp_homo_map' A B).
A, B, C: Group h: B $-> C
Is0Functor (cat_postcomp A h)
A, B, C: Group h: B $-> C
Is0Functor (cat_postcomp A h)
A, B, C: Group h: B $-> C
forallab : A $-> B,
(a $-> b) -> cat_postcomp A h a $-> cat_postcomp A h b
intros [f ?] [g ?] p a ; exact (ap h (p a)).Defined.
A, B, C: Group h: A $-> B
Is0Functor (cat_precomp C h)
A, B, C: Group h: A $-> B
Is0Functor (cat_precomp C h)
A, B, C: Group h: A $-> B
forallab : B $-> C,
(a $-> b) -> cat_precomp C h a $-> cat_precomp C h b
intros [f ?] [g ?] p a ; exact (p (h a)).Defined.(** Group forms a 1Cat *)
Is1Cat Group
Is1Cat Group
by rapply Build_Is1Cat.Defined.(** Under [Funext], the category of groups has morphism extensionality. *)
H: Funext
HasMorExt Group
H: Funext
HasMorExt Group
H: Funext
forall (ab : Group) (fg : a $-> b),
IsEquiv GpdHom_path
intros []; reflexivity.Defined.(** Group isomorphisms become equivalences in the category of groups. *)
HasEquivs Group
HasEquivs Group
Group -> Group -> Type
forallab : Group, (a $-> b) -> Type
forallab : Group, ?CatEquiv' a b -> a $-> b
forall (ab : Group) (f : a $-> b),
?CatIsEquiv' a b f -> ?CatEquiv' a b
forallab : Group, ?CatEquiv' a b -> b $-> a
forall (ab : Group) (f : ?CatEquiv' a b),
?CatIsEquiv' a b (?cate_fun' a b f)
forall (ab : Group) (f : a $-> b)
(fe : ?CatIsEquiv' a b f),
?cate_fun' a b (?cate_buildequiv' a b f fe) $== f
forall (ab : Group) (f : ?CatEquiv' a b),
?cate_inv' a b f $o ?cate_fun' a b f $== Id a
forall (ab : Group) (f : ?CatEquiv' a b),
?cate_fun' a b f $o ?cate_inv' a b f $== Id b
forall (ab : Group) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a -> ?CatIsEquiv' a b f
Group -> Group -> Type
exact GroupIsomorphism.
forallab : Group, (a $-> b) -> Type
exact (funGHf => IsEquiv f).
forallab : Group, GroupIsomorphism a b -> a $-> b
intros G H f; exact f.
forall (ab : Group) (f : a $-> b),
(fun (GH : Group) (f0 : G $-> H) => IsEquiv f0) a b f ->
GroupIsomorphism a b
exact Build_GroupIsomorphism.
forallab : Group, GroupIsomorphism a b -> b $-> a
intros G H; exact grp_iso_inverse.
forall (ab : Group) (f : GroupIsomorphism a b),
(fun (GH : Group) (f0 : G $-> H) => IsEquiv f0) a b
((fun (GH : Group) (f0 : GroupIsomorphism G H) =>
grp_iso_homo G H f0) a b f)
cbn; exact _.
forall (ab : Group) (f : a $-> b)
(fe : (fun (GH : Group) (f0 : G $-> H) => IsEquiv f0)
a b f),
(fun (GH : Group) (f0 : GroupIsomorphism G H) =>
grp_iso_homo G H f0) a b
{| grp_iso_homo := f; isequiv_group_iso := fe |} $==
f
reflexivity.
forall (ab : Group) (f : GroupIsomorphism a b),
(fun (GH : Group) (x : GroupIsomorphism G H) =>
grp_iso_homo H G (grp_iso_inverse x)) a b f $o
(fun (GH : Group) (f0 : GroupIsomorphism G H) =>
grp_iso_homo G H f0) a b f $== Id a
intros ????; apply eissect.
forall (ab : Group) (f : GroupIsomorphism a b),
(fun (GH : Group) (f0 : GroupIsomorphism G H) =>
grp_iso_homo G H f0) a b f $o
(fun (GH : Group) (x : GroupIsomorphism G H) =>
grp_iso_homo H G (grp_iso_inverse x)) a b f $== Id b
intros ????; apply eisretr.
forall (ab : Group) (f : a $-> b) (g : b $-> a),
f $o g $== Id b ->
g $o f $== Id a ->
(fun (GH : Group) (f0 : G $-> H) => IsEquiv f0) a b f
G, H: Group f: G $-> H g: H $-> G p: f $o g $== Id H q: g $o f $== Id G
(fun (GH : Group) (f : G $-> H) => IsEquiv f) G H f
exact (isequiv_adjointify f g p q).Defined.
H: Funext
Is1Cat_Strong Group
H: Funext
Is1Cat_Strong Group
H: Funext
forall (abcd : Group) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o g $o f = h $o (g $o f)
H: Funext
forall (abcd : Group) (f : a $-> b) (g : b $-> c)
(h : c $-> d), h $o (g $o f) = h $o g $o f
H: Funext
forall (ab : Group) (f : a $-> b), Id b $o f = f
H: Funext
forall (ab : Group) (f : a $-> b), f $o Id a = f
all: intros; apply equiv_path_grouphomomorphism; intro; reflexivity.Defined.(** The [group_type] map is a 1-functor. *)
Is0Functor group_type
Is0Functor group_type
forallab : Group, (a $-> b) -> a $-> b
rapply @grp_homo_map.Defined.
Is1Functor group_type
Is1Functor group_type
byapply Build_Is1Functor.Defined.(** The [ptype_group] map is a 1-functor. *)
Is0Functor ptype_group
Is0Functor ptype_group
forallab : Group, (a $-> b) -> a $-> b
rapply @pmap_GroupHomomorphism.Defined.
Is1Functor ptype_group
Is1Functor ptype_group
apply Build_Is1Functor; intros; byapply phomotopy_homotopy_hset.Defined.(** Given a group element [a0 : A] over [b : B], multiplication by [a] establishes an equivalence between the kernel and the fiber over [b]. *)
A, B: Group f: GroupHomomorphism A B b: B
hfiber f b -> hfiber f b <~> hfiber f mon_unit
A, B: Group f: GroupHomomorphism A B b: B
hfiber f b -> hfiber f b <~> hfiber f mon_unit
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b
hfiber f b <~> hfiber f mon_unit
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b
hfiber f b <~> hfiber f (b * - b)
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b
hfiber f b -> hfiber f (b * - b)
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b
IsEquiv ?equiv_fun
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b
hfiber f b -> hfiber f (b * - b)
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b
(funt : B => t * - b) o f ==
f o (funt : A => t * - a0)
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b a: A
f (a * - a0) = f a * - b
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b a: A
f (a * - a0) = f a * - f a0
exact (grp_homo_op f _ _ @ ap (funx => f a * x) (grp_homo_inv f a0)).
A, B: Group f: GroupHomomorphism A B b: B a0: A p: f a0 = b
IsEquiv
(functor_hfiber
((funa : A =>
((grp_homo_op f a (- a0) @
ap (funx : B => f a * x) (grp_homo_inv f a0)) @
ap (funx : B => f a * - x) p)^
:
f a * - b = f (a * - a0))
:
(funt : B => t * - b) o f ==
f o (funt : A => t * - a0)) b)
srapply isequiv_functor_hfiber.Defined.(** ** The trivial group *)
Group
Group
IsGroup Unit
repeatsplit; tryexact _; byintros [].Defined.(** Map out of trivial group. *)
intros ??; symmetry; apply grp_unit_l.Defined.(** Map into trivial group. *)
G: Group
GroupHomomorphism G grp_trivial
G: Group
GroupHomomorphism G grp_trivial
G: Group
G -> grp_trivial
G: Group
IsSemiGroupPreserving ?f
G: Group
IsSemiGroupPreserving (fun_ : G => tt)
intros ??; symmetry; exact (grp_unit_l _).Defined.(** Group is a pointed category. *)
IsPointedCat Group
IsPointedCat Group
Group
IsInitial ?zero_object
IsTerminal ?zero_object
Group
exact grp_trivial.
IsInitial grp_trivial
G: Group
{f : grp_trivial $-> G &
forallg : grp_trivial $-> G, f $== g}
G: Group
forallg : grp_trivial $-> G, grp_trivial_rec G $== g
G: Group g: grp_trivial $-> G
group_unit = g tt
exact (grp_homo_unit g)^.
IsTerminal grp_trivial
G: Group
{f : G $-> grp_trivial &
forallg : G $-> grp_trivial, f $== g}
G: Group
forallg : G $-> grp_trivial,
grp_trivial_corec G $== g
G: Group g: G $-> grp_trivial x: G
tt = g x
apply path_unit.Defined.Definitiongrp_homo_const {GH : Group} : GroupHomomorphism G H
:= zero_morphism.(** ** The direct product of groups *)(** The cartesian product of the underlying sets of two groups has a natural group structure. We call this the direct product of groups. *)
Group -> Group -> Group
Group -> Group -> Group
G, H: Group
Group
G, H: Group
SgOp (G * H)
G, H: Group
MonUnit (G * H)
G, H: Group
Negate (G * H)
G, H: Group
IsGroup (G * H)
(** Operation *)
G, H: Group
SgOp (G * H)
G, H: Group g1: G h1: H g2: G h2: H
(G * H)%type
exact (g1 * g2, h1 * h2).
G, H: Group
MonUnit (G * H)
G, H: Group
Negate (G * H)
G, H: Group
IsGroup (G * H)
(** Unit *)
G, H: Group
Negate (G * H)
G, H: Group
IsGroup (G * H)
(** Inverse *)
G, H: Group
Negate (G * H)
G, H: Group g: G h: H
(G * H)%type
exact (-g, -h).
G, H: Group
IsGroup (G * H)
G, H: Group
IsHSet (G * H)
G, H: Group
Associative sg_op
G, H: Group
LeftIdentity sg_op mon_unit
G, H: Group
RightIdentity sg_op mon_unit
G, H: Group
LeftInverse sg_op negate mon_unit
G, H: Group
RightInverse sg_op negate mon_unit
G, H: Group
Associative sg_op
G, H: Group
LeftIdentity sg_op mon_unit
G, H: Group
RightIdentity sg_op mon_unit
G, H: Group
LeftInverse sg_op negate mon_unit
G, H: Group
RightInverse sg_op negate mon_unit
all: grp_auto.Defined.(** Maps into the direct product can be built by mapping separately into each factor. *)
G, H, K: Group f: GroupHomomorphism K G g: GroupHomomorphism K H
GroupHomomorphism K (grp_prod G H)
G, H, K: Group f: GroupHomomorphism K G g: GroupHomomorphism K H
GroupHomomorphism K (grp_prod G H)
G, H, K: Group f: GroupHomomorphism K G g: GroupHomomorphism K H
K -> grp_prod G H
G, H, K: Group f: GroupHomomorphism K G g: GroupHomomorphism K H
IsSemiGroupPreserving ?f
G, H, K: Group f: GroupHomomorphism K G g: GroupHomomorphism K H
K -> grp_prod G H
exact (funx:K => (f x, g x)).
G, H, K: Group f: GroupHomomorphism K G g: GroupHomomorphism K H
IsSemiGroupPreserving (funx : K => (f x, g x))
G, H, K: Group f: GroupHomomorphism K G g: GroupHomomorphism K H x, y: K
(f (x * y), g (x * y)) = (f x, g x) * (f y, g y)
refine (path_prod' _ _ ); tryapply grp_homo_op.Defined.(** The left factor injects into the direct product. *)Definitiongrp_prod_inl {HK : Group}
: GroupHomomorphism H (grp_prod H K)
:= grp_prod_corec grp_homo_id grp_homo_const.(** The left injection is an embedding. *)
H, K: Group
IsEmbedding grp_prod_inl
H, K: Group
IsEmbedding grp_prod_inl
H, K: Group
isinj grp_prod_inl
H, K: Group h0, h1: H p: (h0, group_unit) = (h1, group_unit)
h0 = h1
exact (fst ((equiv_path_prod _ _)^-1 p)).Defined.(** The right factor injects into the direct product. *)Definitiongrp_prod_inr {HK : Group}
: GroupHomomorphism K (grp_prod H K)
:= grp_prod_corec grp_homo_const grp_homo_id.(** The right injection is an embedding. *)
H, K: Group
IsEmbedding grp_prod_inr
H, K: Group
IsEmbedding grp_prod_inr
H, K: Group
isinj grp_prod_inr
H, K: Group k0, k1: K q: (group_unit, k0) = (group_unit, k1)
k0 = k1
exact (snd ((equiv_path_prod _ _)^-1 q)).Defined.(** Given two pairs of isomorphic groups, their pairwise direct products are isomorphic. *)
A, B, C, D: Group
A ≅ B -> C ≅ D -> grp_prod A C ≅ grp_prod B D
A, B, C, D: Group
A ≅ B -> C ≅ D -> grp_prod A C ≅ grp_prod B D
A, B, C, D: Group f: A ≅ B g: C ≅ D
grp_prod A C ≅ grp_prod B D
A, B, C, D: Group f: A ≅ B g: C ≅ D
grp_prod A C <~> grp_prod B D
A, B, C, D: Group f: A ≅ B g: C ≅ D
IsSemiGroupPreserving ?f
A, B, C, D: Group f: A ≅ B g: C ≅ D
IsSemiGroupPreserving equiv_functor_prod
A, B, C, D: Group f: A ≅ B g: C ≅ D
IsSemiGroupPreserving (functor_prod f g)
A, B, C, D: Group f: A ≅ B g: C ≅ D
IsSemiGroupPreserving
(funz : A * C => (f (fst z), g (snd z)))
A, B, C, D: Group f: A ≅ B g: C ≅ D x, y: (A * C)%type
(f (fst (x * y)), g (snd (x * y))) =
(f (fst x), g (snd x)) * (f (fst y), g (snd y))
A, B, C, D: Group f: A ≅ B g: C ≅ D x, y: (A * C)%type
fst (f (fst (x * y)), g (snd (x * y))) =
fst ((f (fst x), g (snd x)) * (f (fst y), g (snd y)))
A, B, C, D: Group f: A ≅ B g: C ≅ D x, y: (A * C)%type
snd (f (fst (x * y)), g (snd (x * y))) =
snd ((f (fst x), g (snd x)) * (f (fst y), g (snd y)))
1,2: apply grp_homo_op.Defined.(** The first projection of the direct product. *)
G, H: Group
GroupHomomorphism (grp_prod G H) G
G, H: Group
GroupHomomorphism (grp_prod G H) G
G, H: Group
grp_prod G H -> G
G, H: Group
IsSemiGroupPreserving ?f
G, H: Group
IsSemiGroupPreserving fst
intros ? ?; reflexivity.Defined.(** The first projection is a surjection. *)Global Instanceissurj_grp_prod_pr1 {GH : Group}
: IsSurjection (@grp_prod_pr1 G H)
:= issurj_retr grp_prod_inl (fun_ => idpath).(** The second projection of the direct product. *)
G, H: Group
GroupHomomorphism (grp_prod G H) H
G, H: Group
GroupHomomorphism (grp_prod G H) H
G, H: Group
grp_prod G H -> H
G, H: Group
IsSemiGroupPreserving ?f
G, H: Group
IsSemiGroupPreserving snd
intros ? ?; reflexivity.Defined.(** The second projection is a surjection. *)Global Instanceissurj_grp_prod_pr2 {GH : Group}
: IsSurjection (@grp_prod_pr2 G H)
:= issurj_retr grp_prod_inr (fun_ => idpath).(** [Group] is a category with binary products given by the direct product. *)
HasBinaryProducts Group
HasBinaryProducts Group
G, H: Group
BinaryProduct G H
G, H: Group
Group
G, H: Group
?cat_binprod $-> G
G, H: Group
?cat_binprod $-> H
G, H: Group
forallz : Group,
(z $-> G) -> (z $-> H) -> z $-> ?cat_binprod
G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
?cat_pr1 $o ?cat_binprod_corec z f g $== f
G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
?cat_pr2 $o ?cat_binprod_corec z f g $== g
G, H: Group
forall (z : Group) (fg : z $-> ?cat_binprod),
?cat_pr1 $o f $== ?cat_pr1 $o g ->
?cat_pr2 $o f $== ?cat_pr2 $o g -> f $== g
G, H: Group
Group
exact (grp_prod G H).
G, H: Group
grp_prod G H $-> G
exact grp_prod_pr1.
G, H: Group
grp_prod G H $-> H
exact grp_prod_pr2.
G, H: Group
forallz : Group,
(z $-> G) -> (z $-> H) -> z $-> grp_prod G H
G, H, K: Group
(K $-> G) -> (K $-> H) -> K $-> grp_prod G H
exact grp_prod_corec.
G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
grp_prod_pr1 $o
(funK : Group => grp_prod_corec) z f g $== f
G, H, K: Group f: K $-> G g: K $-> H
grp_prod_pr1 $o
(funK : Group => grp_prod_corec) K f g $== f
exact (Id _).
G, H: Group
forall (z : Group) (f : z $-> G) (g : z $-> H),
grp_prod_pr2 $o
(funK : Group => grp_prod_corec) z f g $== g
G, H, K: Group f: K $-> G g: K $-> H
grp_prod_pr2 $o
(funK : Group => grp_prod_corec) K f g $== g
exact (Id _).
G, H: Group
forall (z : Group) (fg : z $-> grp_prod G H),
grp_prod_pr1 $o f $== grp_prod_pr1 $o g ->
grp_prod_pr2 $o f $== grp_prod_pr2 $o g -> f $== g
G, H, K: Group f, g: K $-> grp_prod G H p: grp_prod_pr1 $o f $== grp_prod_pr1 $o g q: grp_prod_pr2 $o f $== grp_prod_pr2 $o g a: K
f a = g a
exact (path_prod' (p a) (q a)).Defined.(** *** Properties of maps to and from the trivial group *)
IsInitial grp_trivial
IsInitial grp_trivial
G: Group
{f : grp_trivial $-> G &
forallg : grp_trivial $-> G, f $== g}
G: Group
forallg : grp_trivial $-> G, grp_trivial_rec G $== g
G: Group g: grp_trivial $-> G
grp_trivial_rec G tt = g tt
apply (grp_homo_unit g)^.Defined.
H: Funext G: Group
Contr (GroupHomomorphism grp_trivial G)
H: Funext G: Group
Contr (GroupHomomorphism grp_trivial G)
H: Funext G: Group
GroupHomomorphism grp_trivial G
H: Funext G: Group
forally : GroupHomomorphism grp_trivial G,
?center = y
H: Funext G: Group
forally : GroupHomomorphism grp_trivial G,
grp_trivial_rec G = y
H: Funext G: Group g: GroupHomomorphism grp_trivial G
grp_trivial_rec G = g
H: Funext G: Group g: GroupHomomorphism grp_trivial G
grp_trivial_rec G == g
H: Funext G: Group g: GroupHomomorphism grp_trivial G
grp_trivial_rec G tt = g tt
H: Funext G: Group g: GroupHomomorphism grp_trivial G
g tt = grp_trivial_rec G tt
rapply grp_homo_unit.Defined.
IsTerminal grp_trivial
IsTerminal grp_trivial
G: Group
{f : G $-> grp_trivial &
forallg : G $-> grp_trivial, f $== g}
G: Group
forallg : G $-> grp_trivial,
grp_trivial_corec G $== g
G: Group g: G $-> grp_trivial x: G
grp_trivial_corec G x = g x
apply path_contr.Defined.
H: Funext G: Group
Contr (GroupHomomorphism G grp_trivial)
H: Funext G: Group
Contr (GroupHomomorphism G grp_trivial)
H: Funext G: Group
GroupHomomorphism G grp_trivial
H: Funext G: Group
forally : GroupHomomorphism G grp_trivial,
?center = y
H: Funext G: Group
forally : GroupHomomorphism G grp_trivial,
(isterminal_grp_trivial G).1 = y
H: Funext G: Group g: GroupHomomorphism G grp_trivial
(isterminal_grp_trivial G).1 = g
H: Funext G: Group g: GroupHomomorphism G grp_trivial
(isterminal_grp_trivial G).1 == g
H: Funext G: Group g: GroupHomomorphism G grp_trivial x: G
(isterminal_grp_trivial G).1 x = g x
apply path_contr.Defined.
H: Funext G: Group
IsHProp (G ≅ grp_trivial)
H: Funext G: Group
IsHProp (G ≅ grp_trivial)
H: Funext G: Group
forallxy : G ≅ grp_trivial, x = y
H: Funext G: Group f, g: G ≅ grp_trivial
f = g
apply equiv_path_groupisomorphism; intro; apply path_ishprop.Defined.(** ** Free groups *)DefinitionFactorsThroughFreeGroup (S : Type) (F_S : Group)
(i : S -> F_S) (A : Group) (g : S -> A) : Type
:= {f : F_S $-> A & f o i == g}.(** Universal property of a free group on a set (type). *)ClassIsFreeGroupOn (S : Type) (F_S : Group) (i : S -> F_S)
:= contr_isfreegroupon : forall (A : Group) (g : S -> A),
Contr (FactorsThroughFreeGroup S F_S i A g).Global Existing Instancecontr_isfreegroupon.(** A group is free if there exists a generating type on which it is a free group. *)ClassIsFreeGroup (F_S : Group)
:= isfreegroup : {S : _ & {i : _ & IsFreeGroupOn S F_S i}}.Global Instanceisfreegroup_isfreegroupon (S : Type) (F_S : Group) (i : S -> F_S)
{H : IsFreeGroupOn S F_S i}
: IsFreeGroup F_S
:= (S; i; H).(** ** Further properties of group homomorphisms. *)(** Characterisation of injective group homomorphisms. *)
A, B: Group f: A $-> B
(foralla : A, f a = group_unit -> a = group_unit) <->
IsEmbedding f
A, B: Group f: A $-> B
(foralla : A, f a = group_unit -> a = group_unit) <->
IsEmbedding f
A, B: Group f: A $-> B
(foralla : A, f a = group_unit -> a = group_unit) ->
IsEmbedding f
A, B: Group f: A $-> B
IsEmbedding f ->
foralla : A, f a = group_unit -> a = group_unit
A, B: Group f: A $-> B
(foralla : A, f a = group_unit -> a = group_unit) ->
IsEmbedding f
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B
IsHProp (hfiber f b)
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B
forallxy : hfiber f b, x = y
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B a0: A p0: f a0 = b a1: A p1: f a1 = b
(a0; p0) = (a1; p1)
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B a0: A p0: f a0 = b a1: A p1: f a1 = b
a0 = a1
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B a0: A p0: f a0 = b a1: A p1: f a1 = b
a0 * - a1 = mon_unit
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B a0: A p0: f a0 = b a1: A p1: f a1 = b
f (a0 * - a1) = group_unit
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B a0: A p0: f a0 = b a1: A p1: f a1 = b
f a0 * - f a1 = group_unit
A, B: Group f: A $-> B h: foralla : A, f a = group_unit -> a = group_unit b: B a0: A p0: f a0 = b a1: A p1: f a1 = b
b * - b = group_unit
apply right_inverse.
A, B: Group f: A $-> B
IsEmbedding f ->
foralla : A, f a = group_unit -> a = group_unit
A, B: Group f: A $-> B E: IsEmbedding f a: A p: f a = group_unit
a = group_unit
A, B: Group f: A $-> B E: IsEmbedding f a: A p: f a = group_unit
f a = f group_unit
exact (p @ (grp_homo_unit f)^).Defined.(** Commutativity can be transferred across isomorphisms. *)
G, H: Group C: Commutative group_sgop f: GroupIsomorphism G H
Commutative group_sgop
G, H: Group C: Commutative group_sgop f: GroupIsomorphism G H
Commutative group_sgop
G, H: Group C: Commutative group_sgop f: GroupIsomorphism G H
forallxy : H, group_sgop x y = group_sgop y x
G, H: Group C: Commutative group_sgop f: GroupIsomorphism G H g1: G
forally : H,
group_sgop (f g1) y = group_sgop y (f g1)
G, H: Group C: Commutative group_sgop f: GroupIsomorphism G H g1, g2: G