Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Spaces.Nat.Core Spaces.Int.
Require Export Classes.interfaces.canonical_names (Zero, zero, Plus, plus, Negate, negate, Involutive, involutive).
Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
Require Export Algebra.Groups.Group.
Require Export Algebra.Groups.Subgroup.
Require Import Algebra.Groups.QuotientGroup.
Require Import WildCat.

Local Set Polymorphic Inductive Cumulativity.

Local Open Scope mc_scope.
Local Open Scope mc_add_scope.

(** * Abelian groups *)

(** Definition of an abelian group *)

Record AbGroup := {
  abgroup_group : Group;
  abgroup_commutative :: @Commutative abgroup_group _ (+);
}.

Coercion abgroup_group : AbGroup >-> Group.

Definition zero_abgroup (A : AbGroup) : Zero A := mon_unit.
Definition negate_abgroup (A : AbGroup) : Negate A := inv.
Definition plus_abgroup (A : AbGroup) : Plus A := sg_op.

(** Sometimes we want an abelian group to act as if it has a [Plus], [Zero] and [Negate] operation. For example, when working with rings. We therefore make this module of hints available for import so that consumers can control the way the abelian group operation is treated.

Files about abelian groups (apart from this one) typically don't have these instances available, whereas files about rings do. *)
Module Import AdditiveInstances.
  #[export] Hint Immediate zero_abgroup : typeclass_instances.
  #[export] Hint Immediate negate_abgroup : typeclass_instances.
  #[export] Hint Immediate plus_abgroup : typeclass_instances.
End AdditiveInstances.

Instance isabgroup_abgroup {A : AbGroup} : IsAbGroup A.
A: AbGroup
IsAbGroup A
Proof.
A: AbGroup
IsAbGroup A
  split; exact _.
Defined.

(** Easier way to build abelian groups without redundant information. *)
Definition Build_AbGroup' (G : Type)
  `{MonUnit G, Inverse G, SgOp G, IsHSet G}
  (comm : Commutative (A:=G) (+))
  (assoc : Associative (A:=G) (+))
  (unit_l : LeftIdentity (A:=G) (+) 0)
  (inv_l : LeftInverse (A:=G) (+) (-) 0)
  : AbGroup.
G: Type
H: MonUnit G
H0: Inverse G
H1: SgOp G
IsHSet0: IsHSet G
comm: Commutative sg_op
assoc: Associative sg_op
unit_l: LeftIdentity sg_op 0
inv_l: LeftInverse sg_op inv 0
AbGroup
Proof.
G: Type
H: MonUnit G
H0: Inverse G
H1: SgOp G
IsHSet0: IsHSet G
comm: Commutative sg_op
assoc: Associative sg_op
unit_l: LeftIdentity sg_op 0
inv_l: LeftInverse sg_op inv 0
AbGroup
  snapply Build_AbGroup.
G: Type
H: MonUnit G
H0: Inverse G
H1: SgOp G
IsHSet0: IsHSet G
comm: Commutative sg_op
assoc: Associative sg_op
unit_l: LeftIdentity sg_op 0
inv_l: LeftInverse sg_op inv 0
Group
G: Type
H: MonUnit G
H0: Inverse G
H1: SgOp G
IsHSet0: IsHSet G
comm: Commutative sg_op
assoc: Associative sg_op
unit_l: LeftIdentity sg_op 0
inv_l: LeftInverse sg_op inv 0
Commutative sg_op
  -
G: Type
H: MonUnit G
H0: Inverse G
H1: SgOp G
IsHSet0: IsHSet G
comm: Commutative sg_op
assoc: Associative sg_op
unit_l: LeftIdentity sg_op 0
inv_l: LeftInverse sg_op inv 0
Group rapply (Build_Group' G).
  -
G: Type
H: MonUnit G
H0: Inverse G
H1: SgOp G
IsHSet0: IsHSet G
comm: Commutative sg_op
assoc: Associative sg_op
unit_l: LeftIdentity sg_op 0
inv_l: LeftInverse sg_op inv 0
Commutative sg_op exact comm.
Defined.

Definition issig_abgroup : _ <~> AbGroup := ltac:(issig).

Definition ab_neg_op {A : AbGroup} (x y : A) : - (x + y) = -x - y.
A: AbGroup
x, y: A
- (x + y) = - x - y
Proof.
A: AbGroup
x, y: A
- (x + y) = - x - y
  lhs napply grp_inv_op.
A: AbGroup
x, y: A
- y - x = - x - y
  apply commutativity.
Defined.

(** ** Paths between abelian groups *)

Definition equiv_path_abgroup `{Univalence} {A B : AbGroup@{u}}
  : GroupIsomorphism A B <~> (A = B).
H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~> A = B
Proof.
H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~> A = B
  refine (equiv_ap_inv issig_abgroup _ _ oE _).
H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~>
issig_abgroup^-1 A = issig_abgroup^-1 B
  refine (equiv_path_sigma_hprop _ _ oE _).
H: Univalence
A, B: AbGroup
GroupIsomorphism A B <~>
(issig_abgroup^-1 A).1 = (issig_abgroup^-1 B).1
  exact equiv_path_group.
Defined.

Definition equiv_path_abgroup_group `{Univalence} {A B : AbGroup}
  : (A = B :> AbGroup) <~> (A = B :> Group)
  := equiv_path_group oE equiv_path_abgroup^-1.

(** ** Subgroups of abelian groups *)

Local Hint Immediate canonical_names.inverse_is_negate : typeclass_instances.

(** Subgroups of abelian groups are abelian *)
Instance isabgroup_subgroup (G : AbGroup) (H : Subgroup G)
  : IsAbGroup H.
G: AbGroup
H: Subgroup G
IsAbGroup H
Proof.
G: AbGroup
H: Subgroup G
IsAbGroup H
  napply Build_IsAbGroup.
G: AbGroup
H: Subgroup G
IsGroup H
G: AbGroup
H: Subgroup G
Commutative group_sgop
  1: exact _.
G: AbGroup
H: Subgroup G
Commutative group_sgop
  intros x y.
G: AbGroup
H: Subgroup G
x, y: H
group_sgop x y = group_sgop y x
  apply path_sigma_hprop.
G: AbGroup
H: Subgroup G
x, y: H
(group_sgop x y).1 = (group_sgop y x).1
  cbn.
G: AbGroup
H: Subgroup G
x, y: H
x.1 + y.1 = y.1 + x.1 apply commutativity.
Defined.

(** Given any subgroup of an abelian group, we can coerce it to an abelian group. Note that Coq complains this coercion doesn't satisfy the uniform-inheritance condition, but in practice it works and doesn't cause any issue, so we ignore it. *)
Definition abgroup_subgroup (G : AbGroup) : Subgroup G -> AbGroup
  := fun H => Build_AbGroup H _.
#[warnings="-uniform-inheritance"]
Coercion abgroup_subgroup : Subgroup >-> AbGroup.

Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G)
  : IsNormalSubgroup H.
G: AbGroup
H: Subgroup G
IsNormalSubgroup H
Proof.
G: AbGroup
H: Subgroup G
IsNormalSubgroup H
  intros x y h.
G: AbGroup
H: Subgroup G
x, y: G
h: H (x + y)
H (y + x)
  by rewrite commutativity.
Defined.

(** ** Quotients of abelian groups *)

Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
  : IsAbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)).
G: AbGroup
H: Subgroup G
IsAbGroup
  (QuotientGroup' G H (isnormal_ab_subgroup G H))
Proof.
G: AbGroup
H: Subgroup G
IsAbGroup
  (QuotientGroup' G H (isnormal_ab_subgroup G H))
  napply Build_IsAbGroup.
G: AbGroup
H: Subgroup G
IsGroup
  (QuotientGroup' G H (isnormal_ab_subgroup G H))
G: AbGroup
H: Subgroup G
Commutative group_sgop
  1: exact _.
G: AbGroup
H: Subgroup G
Commutative group_sgop
  srapply Quotient_ind2_hprop; intros x y.
G: AbGroup
H: Subgroup G
x, y: G
(fun
   x
    y : G /
        in_cosetL
          {|
            normalsubgroup_subgroup := H;
            normalsubgroup_isnormal :=
              isnormal_ab_subgroup G H
          |} => group_sgop x y = group_sgop y x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup G H
        |}) x)
  (class_of
     (in_cosetL
        {|
          normalsubgroup_subgroup := H;
          normalsubgroup_isnormal :=
            isnormal_ab_subgroup G H
        |}) y)
  apply (ap (class_of _)).
G: AbGroup
H: Subgroup G
x, y: G
x + y = y + x
  apply commutativity.
Defined.

Definition QuotientAbGroup (G : AbGroup) (H : Subgroup G) : AbGroup
  := (Build_AbGroup (QuotientGroup' G H (isnormal_ab_subgroup G H)) _).

Arguments QuotientAbGroup G H : simpl never.

Definition quotient_abgroup_rec {G : AbGroup}
  (N : Subgroup G) (H : AbGroup)
  (f : GroupHomomorphism G H) (h : forall n : G, N n -> f n = mon_unit)
  : GroupHomomorphism (QuotientAbGroup G N) H
  := grp_quotient_rec G (Build_NormalSubgroup G N _) f h.

Theorem equiv_quotient_abgroup_ump {F : Funext} {G : AbGroup}
  (N : Subgroup G) (H : Group)
  : {f : GroupHomomorphism G H & forall (n : G), N n -> f n = mon_unit}
    <~> (GroupHomomorphism (QuotientAbGroup G N) H).
F: Funext
G: AbGroup
N: Subgroup G
H: Group
{f : GroupHomomorphism G H &
forall n : G, N n -> f n = 0} <~>
GroupHomomorphism (QuotientAbGroup G N) H
Proof.
F: Funext
G: AbGroup
N: Subgroup G
H: Group
{f : GroupHomomorphism G H &
forall n : G, N n -> f n = 0} <~>
GroupHomomorphism (QuotientAbGroup G N) H
  exact (equiv_grp_quotient_ump (Build_NormalSubgroup G N _) _).
Defined.

(** ** The wild category of abelian groups *)

Instance isgraph_abgroup : IsGraph AbGroup
  := isgraph_induced abgroup_group.

Instance is01cat_abgroup : Is01Cat AbGroup
  := is01cat_induced abgroup_group.

Instance is2graph_abgroup : Is2Graph AbGroup
  := is2graph_induced abgroup_group.

Instance isgraph_abgrouphomomorphism {A B : AbGroup} : IsGraph (A $-> B)
  := is2graph_induced abgroup_group A B.

Instance is01cat_abgrouphomomorphism {A B : AbGroup} : Is01Cat (A $-> B)
  := is01cat_induced (@grp_homo_map A B).

Instance is0gpd_abgrouphomomorphism {A B : AbGroup} : Is0Gpd (A $-> B)
  := is0gpd_induced (@grp_homo_map A B).

(** [AbGroup] forms a 1Cat *)
Instance is1cat_abgroup : Is1Cat AbGroup
  := is1cat_induced _.

Instance hasmorext_abgroup `{Funext} : HasMorExt AbGroup
  := hasmorext_induced _.

Instance hasequivs_abgroup : HasEquivs AbGroup
  := hasequivs_induced _.

(** Zero object of [AbGroup] *)

Definition abgroup_trivial : AbGroup.
AbGroup
Proof.
AbGroup
  rapply (Build_AbGroup grp_trivial).
Commutative sg_op
  by intros [].
Defined.

(** [AbGroup] is a pointed category *)
Instance ispointedcat_abgroup : IsPointedCat AbGroup.
IsPointedCat AbGroup
Proof.
IsPointedCat AbGroup
  apply Build_IsPointedCat with abgroup_trivial.
IsInitial abgroup_trivial
IsTerminal abgroup_trivial
  all: intro A; apply ispointedcat_group.
Defined.

(** [abgroup_group] is a functor *)
Instance is0functor_abgroup_group : Is0Functor abgroup_group
  := is0functor_induced _.

Instance is1functor_abgroup_group : Is1Functor abgroup_group
  := is1functor_induced _.

(** Image of group homomorphisms between abelian groups *)
Definition abgroup_image {A B : AbGroup} (f : A $-> B) : AbGroup
  := Build_AbGroup (grp_image f) _.

(** First isomorphism theorem of abelian groups *)
Definition abgroup_first_iso `{Funext} {A B : AbGroup} (f : A $-> B)
  : GroupIsomorphism (QuotientAbGroup A (grp_kernel f)) (abgroup_image f).
H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  (abgroup_image f)
Proof.
H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  (abgroup_image f)
  etransitivity.
H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  ?Goal
H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism ?Goal (abgroup_image f)
  2: rapply grp_first_iso.
H: Funext
A, B: AbGroup
f: A $-> B
GroupIsomorphism (QuotientAbGroup A (grp_kernel f))
  (QuotientGroup A (grp_kernel f))
  apply grp_iso_quotient_normal.
Defined.

(** ** Kernels of abelian groups *)

Definition ab_kernel {A B : AbGroup} (f : A $-> B) : AbGroup
  := Build_AbGroup (grp_kernel f) _.

(** ** Transporting in families related to abelian groups *)

Lemma transport_abgrouphomomorphism_from_const `{Univalence} {A B B' : AbGroup}
      (p : B = B') (f : GroupHomomorphism A B)
  : transport (Hom A) p f
    = grp_homo_compose (equiv_path_abgroup^-1 p) f.
H: Univalence
A, B, B': AbGroup
p: B = B'
f: GroupHomomorphism A B
transport (Hom A) p f =
grp_homo_compose (equiv_path_abgroup^-1 p) f
Proof.
H: Univalence
A, B, B': AbGroup
p: B = B'
f: GroupHomomorphism A B
transport (Hom A) p f =
grp_homo_compose (equiv_path_abgroup^-1 p) f
  induction p.
H: Univalence
A, B: AbGroup
f: GroupHomomorphism A B
transport (Hom A) 1 f =
grp_homo_compose (equiv_path_abgroup^-1 1%path) f
  by apply equiv_path_grouphomomorphism.
Defined.

Lemma transport_iso_abgrouphomomorphism_from_const `{Univalence} {A B B' : AbGroup}
      (phi : GroupIsomorphism B B') (f : GroupHomomorphism A B)
  : transport (Hom A) (equiv_path_abgroup phi) f
    = grp_homo_compose phi f.
H: Univalence
A, B, B': AbGroup
phi: GroupIsomorphism B B'
f: GroupHomomorphism A B
transport (Hom A) (equiv_path_abgroup phi) f =
grp_homo_compose phi f
Proof.
H: Univalence
A, B, B': AbGroup
phi: GroupIsomorphism B B'
f: GroupHomomorphism A B
transport (Hom A) (equiv_path_abgroup phi) f =
grp_homo_compose phi f
  refine (transport_abgrouphomomorphism_from_const _ _ @ _).
H: Univalence
A, B, B': AbGroup
phi: GroupIsomorphism B B'
f: GroupHomomorphism A B
grp_homo_compose
  (equiv_path_abgroup^-1 (equiv_path_abgroup phi)) f =
grp_homo_compose phi f
  by rewrite eissect.
Defined.

Lemma transport_abgrouphomomorphism_to_const `{Univalence} {A A' B : AbGroup}
      (p : A = A') (f : GroupHomomorphism A B)
  : transport (fun G => Hom G B) p f
    = grp_homo_compose f (grp_iso_inverse (equiv_path_abgroup^-1 p)).
H: Univalence
A, A', B: AbGroup
p: A = A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B) p f =
grp_homo_compose f
  (grp_iso_inverse (equiv_path_abgroup^-1 p))
Proof.
H: Univalence
A, A', B: AbGroup
p: A = A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B) p f =
grp_homo_compose f
  (grp_iso_inverse (equiv_path_abgroup^-1 p))
  induction p; cbn.
H: Univalence
A, B: AbGroup
f: GroupHomomorphism A B
f =
grp_homo_compose f
  {|
    grp_homo_map := idmap;
    issemigrouppreserving_grp_homo :=
      abstract_algebra.invert_sg_morphism idmap
        abstract_algebra.id_sg_morphism
  |}
  by apply equiv_path_grouphomomorphism.
Defined.

Lemma transport_iso_abgrouphomomorphism_to_const `{Univalence} {A A' B : AbGroup}
      (phi : GroupIsomorphism A A') (f : GroupHomomorphism A B)
  : transport (fun G => Hom G B) (equiv_path_abgroup phi) f
    = grp_homo_compose f (grp_iso_inverse phi).
H: Univalence
A, A', B: AbGroup
phi: GroupIsomorphism A A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B)
  (equiv_path_abgroup phi) f =
grp_homo_compose f (grp_iso_inverse phi)
Proof.
H: Univalence
A, A', B: AbGroup
phi: GroupIsomorphism A A'
f: GroupHomomorphism A B
transport (fun G : AbGroup => G $-> B)
  (equiv_path_abgroup phi) f =
grp_homo_compose f (grp_iso_inverse phi)
  refine (transport_abgrouphomomorphism_to_const _ _ @ _).
H: Univalence
A, A', B: AbGroup
phi: GroupIsomorphism A A'
f: GroupHomomorphism A B
grp_homo_compose f
  (grp_iso_inverse
     (equiv_path_abgroup^-1 (equiv_path_abgroup phi))) =
grp_homo_compose f (grp_iso_inverse phi)
  by rewrite eissect.
Defined.

(** ** Operations on abelian groups *)

(** The negation automorphism of an abelian group *)
Definition ab_homo_negation {A : AbGroup} : GroupIsomorphism A A.
A: AbGroup
GroupIsomorphism A A
Proof.
A: AbGroup
GroupIsomorphism A A
  snapply Build_GroupIsomorphism.
A: AbGroup
GroupHomomorphism A A
A: AbGroup
IsEquiv ?grp_iso_homo
  -
A: AbGroup
GroupHomomorphism A A snapply Build_GroupHomomorphism.
A: AbGroup
A -> A
A: AbGroup
IsSemiGroupPreserving ?grp_homo_map
    +
A: AbGroup
A -> A exact (fun a => -a).
    +
A: AbGroup
IsSemiGroupPreserving (fun a : A => - a) intros x y.
A: AbGroup
x, y: A
- (x + y) = - x - y
      refine (grp_inv_op x y @ _).
A: AbGroup
x, y: A
- y - x = - x - y
      apply commutativity.
  -
A: AbGroup
IsEquiv
  {|
    grp_homo_map := fun a : A => - a;
    issemigrouppreserving_grp_homo :=
      (fun x y : A =>
       grp_inv_op x y @ commutativity (- y) (- x))
      :
      IsSemiGroupPreserving (fun a : A => - a)
  |} srapply isequiv_adjointify.
A: AbGroup
A -> A
A: AbGroup
{|
  grp_homo_map := fun a : A => - a;
  issemigrouppreserving_grp_homo :=
    (fun x y : A =>
     grp_inv_op x y @ commutativity (- y) (- x))
    :
    IsSemiGroupPreserving (fun a : A => - a)
|} o ?g == idmap
A: AbGroup
?g
o {|
    grp_homo_map := fun a : A => - a;
    issemigrouppreserving_grp_homo :=
      (fun x y : A =>
       grp_inv_op x y @ commutativity (- y) (- x))
      :
      IsSemiGroupPreserving (fun a : A => - a)
  |} == idmap
    1: exact (fun a => -a).
A: AbGroup
{|
  grp_homo_map := fun a : A => - a;
  issemigrouppreserving_grp_homo :=
    (fun x y : A =>
     grp_inv_op x y @ commutativity (- y) (- x))
    :
    IsSemiGroupPreserving (fun a : A => - a)
|} o (fun a : A => - a) == idmap
A: AbGroup
(fun a : A => - a)
o {|
    grp_homo_map := fun a : A => - a;
    issemigrouppreserving_grp_homo :=
      (fun x y : A =>
       grp_inv_op x y @ commutativity (- y) (- x))
      :
      IsSemiGroupPreserving (fun a : A => - a)
  |} == idmap
    1-2: exact inverse_involutive.
Defined.

(** Multiplication by [n : Int] defines an endomorphism of any abelian group [A]. *)
Definition ab_mul {A : AbGroup} (n : Int) : GroupHomomorphism A A.
A: AbGroup
n: Int
GroupHomomorphism A A
Proof.
A: AbGroup
n: Int
GroupHomomorphism A A
  snapply Build_GroupHomomorphism.
A: AbGroup
n: Int
A -> A
A: AbGroup
n: Int
IsSemiGroupPreserving ?grp_homo_map
  1: exact (fun a => grp_pow a n).
A: AbGroup
n: Int
IsSemiGroupPreserving (fun a : A => grp_pow a n)
  intros a b.
A: AbGroup
n: Int
a, b: A
grp_pow (a + b) n = grp_pow a n + grp_pow b n
  apply grp_pow_mul, commutativity.
Defined.

(** [ab_mul n] is natural. *)
Definition ab_mul_natural {A B : AbGroup}
  (f : GroupHomomorphism A B) (n : Int)
  : f o ab_mul n == ab_mul n o f
  := grp_pow_natural f n.

(** The image of an inclusion is a normal subgroup. *)
Definition ab_image_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f} : NormalSubgroup B
  := {| normalsubgroup_subgroup := grp_image_embedding f; normalsubgroup_isnormal := _ |}.

Definition ab_image_in_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f}
  : GroupIsomorphism A (ab_image_embedding f)
  := grp_image_in_embedding f.

(** The cokernel of a homomorphism into an abelian group. *)
Definition ab_cokernel {G : Group@{u}} {A : AbGroup@{u}} (f : GroupHomomorphism G A)
  : AbGroup := QuotientAbGroup _ (grp_image f).

Definition ab_cokernel_embedding {G : Group} {A : AbGroup} (f : G $-> A) `{IsEmbedding f}
  : AbGroup := QuotientAbGroup _ (grp_image_embedding f).

Definition ab_cokernel_embedding_rec {G: Group} {A B : AbGroup} (f : G $-> A) `{IsEmbedding f}
  (h : A $-> B) (p : grp_homo_compose h f $== grp_homo_const)
  : ab_cokernel_embedding f $-> B.
G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
ab_cokernel_embedding f $-> B
Proof.
G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
ab_cokernel_embedding f $-> B
  snapply (grp_quotient_rec _ _ h).
G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
forall n : A,
{|
  normalsubgroup_subgroup := grp_image_embedding f;
  normalsubgroup_isnormal :=
    isnormal_ab_subgroup A (grp_image_embedding f)
|} n -> h n = 0
  intros a [g q].
G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
a: A
g: G
q: f g = a
h a = 0
  induction q.
G: Group
A, B: AbGroup
f: G $-> A
IsEmbedding0: IsEmbedding f
h: A $-> B
p: grp_homo_compose h f $== grp_homo_const
g: G
h (f g) = 0
  exact (p g).
Defined.