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]
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
SgOp CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
SgOp CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: CongruenceQuotient
CongruenceQuotient -> CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: CongruenceQuotient
G -> CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: CongruenceQuotient
forallx0y : G, R x0 y -> ?pclass x0 = ?pclass y
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: CongruenceQuotient
G -> CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y: G
CongruenceQuotient -> CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y: G
G -> CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y: G
forallxy0 : G, R x y0 -> ?pclass x = ?pclass y0
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y: G
G -> CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y, x: G
CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y, x: G
G
exact (x * y).
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y: G
forallxy0 : G,
R x y0 ->
(funx0 : G => class_of R (x0 * y)) x =
(funx0 : G => class_of R (x0 * y)) y0
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y, a, b: G r: R a b
(funx : G => class_of R (x * y)) a =
(funx : G => class_of R (x * y)) b
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y, a, b: G r: R a b
class_of R (a * y) = class_of R (b * y)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R y, a, b: G r: R a b
R (a * y) (b * y)
byapply iscong.
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: CongruenceQuotient
forallx0y : G,
R x0 y ->
(funy0 : G =>
Quotient_rec R CongruenceQuotient
(funx : G => class_of R (x * y0))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y0))
:
(funx : G => class_of R (x * y0)) a =
(funx : G => class_of R (x * y0)) b) x) x0 =
(funy0 : G =>
Quotient_rec R CongruenceQuotient
(funx : G => class_of R (x * y0))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y0))
:
(funx : G => class_of R (x * y0)) a =
(funx : G => class_of R (x * y0)) b) x) y
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: CongruenceQuotient a, b: G r: R a b
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx : G => class_of R (x * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx : G => class_of R (x * y)) a =
(funx : G => class_of R (x * y)) b) x) a =
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx : G => class_of R (x * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx : G => class_of R (x * y)) a =
(funx : G => class_of R (x * y)) b) x) b
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R a, b: G r: R a b
forallx : CongruenceQuotient,
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx0 : G => class_of R (x0 * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx0 : G => class_of R (x0 * y)) a =
(funx0 : G => class_of R (x0 * y)) b) x) a =
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx0 : G => class_of R (x0 * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx0 : G => class_of R (x0 * y)) a =
(funx0 : G => class_of R (x0 * y)) b) x) b
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R a, b: G r: R a b
forallx : G,
(funq : G / R =>
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx0 : G => class_of R (x0 * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx0 : G => class_of R (x0 * y)) a =
(funx0 : G => class_of R (x0 * y)) b) q) a =
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx0 : G => class_of R (x0 * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx0 : G => class_of R (x0 * y)) a =
(funx0 : G => class_of R (x0 * y)) b) q) b)
(class_of R x)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R a, b: G r: R a b x: G
(funq : G / R =>
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx : G => class_of R (x * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx : G => class_of R (x * y)) a =
(funx : G => class_of R (x * y)) b) q) a =
(funy : G =>
Quotient_rec R CongruenceQuotient
(funx : G => class_of R (x * y))
(fun (ab : G) (r : R a b) =>
qglue (iscong r (Reflexive0 y))
:
(funx : G => class_of R (x * y)) a =
(funx : G => class_of R (x * y)) b) q) b)
(class_of R x)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R a, b: G r: R a b x: G
R (x * a) (x * b)
byapply iscong.Defined.
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
MonUnit CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
MonUnit CongruenceQuotient
apply class_of, mon_unit.Defined.
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
Negate CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
Negate CongruenceQuotient
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
G -> G
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
forallxy : G, R x y -> R (?f x) (?f y)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
forallxy : G, R x y -> R (- x) (- y)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y
R (- x) (- y)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y
R (mon_unit * - x) (- y)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y
R (- y * y * - x) (- y)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y g:= - y * y * - x: G
R g (- y)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y g:= - y * y * - x: G
R g (- y * mon_unit)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y g:= - y * y * - x: G
R g (- y * (x * - x))
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y
R (- y * y * - x) (- y * (x * - x))
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y
R (- y * (y * - x)) (- y * (x * - x))
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y
R (y * - x) (x * - x)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: G p: R x y
R y x
bysymmetry.Defined.
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
Associative congquot_sgop
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
Associative congquot_sgop
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x, y: CongruenceQuotient
forallz : CongruenceQuotient,
congquot_sgop x (congquot_sgop y z) =
congquot_sgop (congquot_sgop x y) z
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: CongruenceQuotient a: G
forally : CongruenceQuotient,
(funq : G / R =>
congquot_sgop x (congquot_sgop y q) =
congquot_sgop (congquot_sgop x y) q) (class_of R a)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R a, b: G
forallx : CongruenceQuotient,
(funq : G / R =>
(funq0 : G / R =>
congquot_sgop x (congquot_sgop q q0) =
congquot_sgop (congquot_sgop x q) q0) (class_of R a))
(class_of R b)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R a, b, c: G
(funq : G / R =>
(funq0 : G / R =>
(funq1 : G / R =>
congquot_sgop q (congquot_sgop q0 q1) =
congquot_sgop (congquot_sgop q q0) q1)
(class_of R a)) (class_of R b)) (class_of R c)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
LeftIdentity congquot_sgop congquot_mon_unit
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
LeftIdentity congquot_sgop congquot_mon_unit
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: G
(funq : G / R =>
congquot_sgop congquot_mon_unit q = q) (class_of R x)
bysimpl; rewrite left_identity.Qed.
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
RightIdentity congquot_sgop congquot_mon_unit
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
RightIdentity congquot_sgop congquot_mon_unit
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: G
(funq : G / R =>
congquot_sgop q congquot_mon_unit = q) (class_of R x)
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: G
(funq : G / R =>
congquot_sgop (congquot_negate q) q =
congquot_mon_unit) (class_of R x)
bysimpl; rewrite left_inverse.Qed.
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R
G: Group R: Relation G is_mere_relation0: is_mere_relation G R IsCongruence0: IsCongruence R Reflexive0: Reflexive R Symmetric0: Symmetric R Transitive0: Transitive R x: G
(funq : G / R =>
congquot_sgop q (congquot_negate q) =
congquot_mon_unit) (class_of R x)
bysimpl; rewrite right_inverse.Qed.Global Instanceisgroup_quotientgroup : IsGroup CongruenceQuotient := {}.EndGroupCongruenceQuotient.(** Now we can define the quotient group by a normal subgroup. *)SectionQuotientGroup.Context (G : Group) (N : NormalSubgroup G).
G: Group N: NormalSubgroup G
IsCongruence (in_cosetL N)
G: Group N: NormalSubgroup G
IsCongruence (in_cosetL N)
G: Group N: NormalSubgroup G
forallxx'yy' : G,
in_cosetL N x x' ->
in_cosetL N y y' -> in_cosetL N (x * y) (x' * y')
intros; byapply in_cosetL_cong.Defined.
G: Group N: NormalSubgroup G
IsCongruence (in_cosetR N)
G: Group N: NormalSubgroup G
IsCongruence (in_cosetR N)
G: Group N: NormalSubgroup G
forallxx'yy' : G,
in_cosetR N x x' ->
in_cosetR N y y' -> in_cosetR N (x * y) (x' * y')
intros; byapply in_cosetR_cong.Defined.(** Now we have to make a choice whether to pick the left or right cosets. Due to existing convention we shall pick left cosets but we note that we could equally have picked right. *)DefinitionQuotientGroup : Group
:= Build_Group (G / (in_cosetL N)) _ _ _ _.
G: Group N: NormalSubgroup G
G $-> QuotientGroup
G: Group N: NormalSubgroup G
G $-> QuotientGroup
G: Group N: NormalSubgroup G
G -> QuotientGroup
G: Group N: NormalSubgroup G
IsSemiGroupPreserving ?f
G: Group N: NormalSubgroup G
IsSemiGroupPreserving (class_of (in_cosetL N))
intros ??; reflexivity.Defined.
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
QuotientGroup $-> A
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
QuotientGroup $-> A
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
QuotientGroup -> A
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
IsSemiGroupPreserving ?f
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
QuotientGroup -> A
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
G -> A
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
forallxy : G,
in_cosetL N x y -> ?pclass x = ?pclass y
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
G -> A
exact f.
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
forallxy : G, in_cosetL N x y -> f x = f y
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x, y: G n: N (- x * y)
f x = f y
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x, y: G n: N (- x * y)
f y = f x
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x, y: G n: N (- x * y)
- f x * f y = mon_unit
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x, y: G n: N (- x * y)
f (- x) * f y = mon_unit
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x, y: G n: N (- x * y)
f (- x * y) = mon_unit
apply h; assumption.
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
IsSemiGroupPreserving
(Quotient_rec (in_cosetL N) A f
((fun (xy : G) (n : N (- x * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y) n)
(grp_homo_op f (- x) y))
(grp_homo_inv f x)))^)
:
forallxy : G, in_cosetL N x y -> f x = f y))
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x: QuotientGroup
forally : QuotientGroup,
Quotient_rec (in_cosetL N) A f
(fun (xy0 : G) (n : N (- x * y0)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y0 = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y0) n) (grp_homo_op f (- x) y0))
(grp_homo_inv f x)))^) (x * y) =
Quotient_rec (in_cosetL N) A f
(fun (xy0 : G) (n : N (- x * y0)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y0 = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y0) n) (grp_homo_op f (- x) y0))
(grp_homo_inv f x)))^) x *
Quotient_rec (in_cosetL N) A f
(fun (xy0 : G) (n : N (- x * y0)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y0 = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y0) n) (grp_homo_op f (- x) y0))
(grp_homo_inv f x)))^) y
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x: QuotientGroup
forallx0 : G,
Quotient_rec (in_cosetL N) A f
(fun (xy : G) (n : N (- x * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y) n) (grp_homo_op f (- x) y))
(grp_homo_inv f x)))^)
(x * class_of (in_cosetL N) x0) =
Quotient_rec (in_cosetL N) A f
(fun (xy : G) (n : N (- x * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y) n) (grp_homo_op f (- x) y))
(grp_homo_inv f x)))^) x *
Quotient_rec (in_cosetL N) A f
(fun (xy : G) (n : N (- x * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y) n) (grp_homo_op f (- x) y))
(grp_homo_inv f x)))^)
(class_of (in_cosetL N) x0)
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit x: QuotientGroup y: G
Quotient_rec (in_cosetL N) A f
(fun (xy : G) (n : N (- x * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y) n) (grp_homo_op f (- x) y))
(grp_homo_inv f x)))^)
(x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
(fun (xy : G) (n : N (- x * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y) n) (grp_homo_op f (- x) y))
(grp_homo_inv f x)))^) x *
Quotient_rec (in_cosetL N) A f
(fun (xy : G) (n : N (- x * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x * y) n) (grp_homo_op f (- x) y))
(grp_homo_inv f x)))^)
(class_of (in_cosetL N) y)
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit y: G
forallx : QuotientGroup,
Quotient_rec (in_cosetL N) A f
(fun (x0y : G) (n : N (- x0 * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x0 * y) n) (grp_homo_op f (- x0) y))
(grp_homo_inv f x0)))^)
(x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
(fun (x0y : G) (n : N (- x0 * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x0 * y) n) (grp_homo_op f (- x0) y))
(grp_homo_inv f x0)))^) x *
Quotient_rec (in_cosetL N) A f
(fun (x0y : G) (n : N (- x0 * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x0 * y) n) (grp_homo_op f (- x0) y))
(grp_homo_inv f x0)))^)
(class_of (in_cosetL N) y)
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit y: G
forallx : G,
Quotient_rec (in_cosetL N) A f
(fun (x0y : G) (n : N (- x0 * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x0 * y) n) (grp_homo_op f (- x0) y))
(grp_homo_inv f x0)))^)
(class_of (in_cosetL N) x * class_of (in_cosetL N) y) =
Quotient_rec (in_cosetL N) A f
(fun (x0y : G) (n : N (- x0 * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x0 * y) n) (grp_homo_op f (- x0) y))
(grp_homo_inv f x0)))^)
(class_of (in_cosetL N) x) *
Quotient_rec (in_cosetL N) A f
(fun (x0y : G) (n : N (- x0 * y)) =>
(letX := equiv_fun grp_moveL_M1 in
X
(internal_paths_rew
(fung : A => g * f y = mon_unit)
(internal_paths_rew
(fung : A => g = mon_unit)
(h (- x0 * y) n) (grp_homo_op f (- x0) y))
(grp_homo_inv f x0)))^)
(class_of (in_cosetL N) y)
G: Group N: NormalSubgroup G A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit y, x: G
f (x * y) = f x * f y
apply grp_homo_op.Defined.EndQuotientGroup.Arguments grp_quotient_map {_ _}.Notation"G / N" := (QuotientGroup G N) : group_scope.(** Rephrasing that lets you specify the normality proof *)DefinitionQuotientGroup' (G : Group) (N : Subgroup G) (H : IsNormalSubgroup N)
:= QuotientGroup G (Build_NormalSubgroup G N H).LocalOpen Scope group_scope.(** Computation rule for grp_quotient_rec. *)
F: Funext G: Group N: NormalSubgroup G H, A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
grp_quotient_rec G N f h $o grp_quotient_map = f
F: Funext G: Group N: NormalSubgroup G H, A: Group f: G $-> A h: foralln : G, N n -> f n = mon_unit
grp_quotient_rec G N f h $o grp_quotient_map = f
apply equiv_path_grouphomomorphism; reflexivity.Defined.(** Computation rule for grp_quotient_rec. *)Definitiongrp_quotient_rec_beta' {G : Group}
(N : NormalSubgroup G) (H : Group)
{A : Group} (f : G $-> A)
(h : foralln:G, N n -> f n = mon_unit)
: (grp_quotient_rec G N f h) $o grp_quotient_map == f
:= fun_ => idpath.(** The proof of normality is irrelevent up to equivalence. This is unfortunate that it doesn't hold definitionally. *)
G: Group H: Subgroup G k, k': IsNormalSubgroup H
QuotientGroup' G H k ≅ QuotientGroup' G H k'
G: Group H: Subgroup G k, k': IsNormalSubgroup H
QuotientGroup' G H k ≅ QuotientGroup' G H k'
G: Group H: Subgroup G k, k': IsNormalSubgroup H
QuotientGroup' G H k <~> QuotientGroup' G H k'
G: Group H: Subgroup G k, k': IsNormalSubgroup H
IsSemiGroupPreserving ?f
G: Group H: Subgroup G k, k': IsNormalSubgroup H
IsSemiGroupPreserving 1%equiv
G: Group H: Subgroup G k, k': IsNormalSubgroup H x: QuotientGroup' G H k
forally : QuotientGroup' G H k,
1%equiv (x * y) = 1%equiv x * 1%equiv y
G: Group H: Subgroup G k, k': IsNormalSubgroup H y: G
forallx : QuotientGroup' G H k,
(funq : Quotient
(in_cosetL
{|
normalsubgroup_subgroup := H;
normalsubgroup_isnormal := k
|}) =>
1%equiv (x * q) = 1%equiv x * 1%equiv q)
(class_of
(in_cosetL
{|
normalsubgroup_subgroup := H;
normalsubgroup_isnormal := k
|}) y)
G: Group H: Subgroup G k, k': IsNormalSubgroup H y, x: G
(funX : {f : G $-> H &
foralln : G, N n -> f n = mon_unit} =>
(fun (f : G $-> H)
(p : foralln : G, N n -> f n = mon_unit) =>
grp_quotient_rec G N f p) X.1 X.2)
o (funf : G / N $-> H =>
(f $o grp_quotient_map;
fun (n : G) (h : N n) =>
ap f
(qglue
(internal_paths_rew_r (fung : G => N g)
(issubgroup_in_inv n h)
(right_identity (- n))
:
in_cosetL N n mon_unit)) @ grp_homo_unit f
:
(f $o grp_quotient_map) n = mon_unit)) == idmap
F: Funext G: Group N: NormalSubgroup G H: Group f: G / N $-> H
grp_quotient_rec G N (f $o grp_quotient_map)
(fun (n : G) (h : N n) =>
ap f
(qglue
(internal_paths_rew_r (fung : G => N g)
(issubgroup_in_inv n h)
(right_identity (- n)))) @ grp_homo_unit f) =
f
F: Funext G: Group N: NormalSubgroup G H: Group f: G / N $-> H
grp_quotient_rec G N (f $o grp_quotient_map)
(fun (n : G) (h : N n) =>
ap f
(qglue
(internal_paths_rew_r (fung : G => N g)
(issubgroup_in_inv n h)
(right_identity (- n)))) @ grp_homo_unit f) ==
f
by srapply Quotient_ind_hprop.
F: Funext G: Group N: NormalSubgroup G H: Group
(funf : G / N $-> H =>
(f $o grp_quotient_map;
fun (n : G) (h : N n) =>
ap f
(qglue
(internal_paths_rew_r (fung : G => N g)
(issubgroup_in_inv n h)
(right_identity (- n))
:
in_cosetL N n mon_unit)) @ grp_homo_unit f
:
(f $o grp_quotient_map) n = mon_unit))
o (funX : {f : G $-> H &
foralln : G, N n -> f n = mon_unit} =>
(fun (f : G $-> H)
(p : foralln : G, N n -> f n = mon_unit) =>
grp_quotient_rec G N f p) X.1 X.2) == idmap
F: Funext G: Group N: NormalSubgroup G H: Group f: G $-> H p: foralln : G, N n -> f n = mon_unit
(grp_quotient_rec G N f p $o grp_quotient_map;
fun (n : G) (h : N n) =>
ap (grp_quotient_rec G N f p)
(qglue
(internal_paths_rew_r (fung : G => N g)
(issubgroup_in_inv n h) (right_identity (- n)))) @
grp_homo_unit (grp_quotient_rec G N f p)) = (f; p)
F: Funext G: Group N: NormalSubgroup G H: Group f: G $-> H p: foralln : G, N n -> f n = mon_unit
grp_homo_compose (grp_quotient_rec G N f p)
grp_quotient_map = f
exact (grp_quotient_rec_beta N H f p).Defined.SectionFirstIso.Context `{Funext} {A B : Group} (phi : A $-> B).(** First we define a map from the quotient by the kernel of phi into the image of phi *)
H: Funext A, B: Group phi: A $-> B
A / grp_kernel phi $-> grp_image phi
H: Funext A, B: Group phi: A $-> B
A / grp_kernel phi $-> grp_image phi
H: Funext A, B: Group phi: A $-> B
A $-> grp_image phi
H: Funext A, B: Group phi: A $-> B
foralln : A, grp_kernel phi n -> ?f n = mon_unit
H: Funext A, B: Group phi: A $-> B
A $-> grp_image phi
srapply grp_image_in.
H: Funext A, B: Group phi: A $-> B
foralln : A,
grp_kernel phi n -> grp_image_in phi n = mon_unit
H: Funext A, B: Group phi: A $-> B n: A x: grp_kernel phi n
grp_image_in phi n = mon_unit
byapply path_sigma_hprop.Defined.(** The underlying map of this homomorphism is an equivalence *)
H: Funext A, B: Group phi: A $-> B x, y: A h: (phi x; tr (x; 1%path)) = (phi y; tr (y; 1%path))
class_of (in_cosetL (grp_kernel phi)) x =
class_of (in_cosetL (grp_kernel phi)) y
H: Funext A, B: Group phi: A $-> B x, y: A h: (phi x; tr (x; 1%path)) = (phi y; tr (y; 1%path))
phi (- x * y) = group_unit
H: Funext A, B: Group phi: A $-> B x, y: A h: phi x = phi y
phi (- x * y) = group_unit
H: Funext A, B: Group phi: A $-> B x, y: A h: phi x = phi y
phi (- x * y) = group_unit
H: Funext A, B: Group phi: A $-> B x, y: A h: phi x = phi y
- phi y * phi y = group_unit
srapply negate_l.Defined.(** First isomorphism theorem for groups *)
H: Funext A, B: Group phi: A $-> B
A / grp_kernel phi ≅ grp_image phi
H: Funext A, B: Group phi: A $-> B
A / grp_kernel phi ≅ grp_image phi
exact (Build_GroupIsomorphism _ _ grp_image_quotient _).Defined.EndFirstIso.(** Quotient groups are finite. *)(** Note that we cannot constructively conclude that the normal subgroup [H] must be finite since [G] is, therefore we keep it as an assumption. *)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
Finite (G / H)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
Finite (G / H)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
Finite G
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
is_mere_relation G (in_cosetL H)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
Reflexive (in_cosetL H)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
Transitive (in_cosetL H)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
Symmetric (in_cosetL H)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
forallxy : G, Decidable (in_cosetL H x y)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H
forallxy : G, Decidable (in_cosetL H x y)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H x, y: G
Decidable (in_cosetL H x y)
U: Univalence G: Group H: NormalSubgroup G fin_G: Finite G fin_H: Finite H x, y: G dec_H:= detachable_finite_subset H: forallx : G, Decidable (H x)
Decidable (in_cosetL H x y)
apply dec_H.Defined.
H: Univalence G: Group N: NormalSubgroup G
GroupIsomorphism N (grp_kernel grp_quotient_map)
H: Univalence G: Group N: NormalSubgroup G
GroupIsomorphism N (grp_kernel grp_quotient_map)
H: Univalence G: Group N: NormalSubgroup G
GroupHomomorphism N (grp_kernel grp_quotient_map)
H: Univalence G: Group N: NormalSubgroup G
IsEquiv ?grp_iso_homo
H: Univalence G: Group N: NormalSubgroup G
GroupHomomorphism N (grp_kernel grp_quotient_map)
H: Univalence G: Group N: NormalSubgroup G
grp_quotient_map $o subgroup_incl N == grp_homo_const
H: Univalence G: Group N: NormalSubgroup G x: N
class_of (funxy : G => N (- x * y)) x.1 =
congquot_mon_unit