Merge pull request #2175 from Alizter/ps/rr/remove_implicit_arguments…

…_in_trivial_subgroup_and_maximal_subgroup remove implicit arguments in trivial_subgroup and maximal_subgroup
HoTT · Jan 3, 2025 · 6c6527d · 6c6527d
2 parents fe2adfe + 298b7ce
commit 6c6527d
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/theories/Algebra/Groups/Kernel.v b/theories/Algebra/Groups/Kernel.v
@@ -57,7 +57,7 @@ Defined.
 
 (** ** Characterisation of group embeddings *)
 Proposition equiv_kernel_isembedding `{Univalence} {A B : Group} (f : A $-> B)
-  : (grp_kernel f = trivial_subgroup :> Subgroup A) <~> IsEmbedding f.
+  : (grp_kernel f = trivial_subgroup A :> Subgroup A) <~> IsEmbedding f.
 Proof.
   refine (_ oE (equiv_path_subgroup' _ _)^-1%equiv).
   apply equiv_iff_hprop_uncurried.

diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v
@@ -52,6 +52,6 @@ Defined.
 (** A complex 0 -> A -> B is purely exact if and only if the kernel of the map A -> B is trivial. *)
 Definition equiv_grp_isexact_kernel `{Univalence} {A B : Group} (f : A $-> B)
   : IsExact purely (grp_trivial_rec A) f
-      <~> (grp_kernel f = trivial_subgroup :> Subgroup _)
+      <~> (grp_kernel f = trivial_subgroup A :> Subgroup _)
   := (equiv_kernel_isembedding f)^-1%equiv
        oE equiv_iff_hprop_uncurried (iff_grp_isexact_isembedding f).
diff --git a/theories/Algebra/Groups/Subgroup.v b/theories/Algebra/Groups/Subgroup.v
@@ -178,7 +178,7 @@ Definition issig_subgroup {G : Group} : _ <~> Subgroup G
   := ltac:(issig).
 
 (** Trivial subgroup *)
-Definition trivial_subgroup {G} : Subgroup G.
+Definition trivial_subgroup G : Subgroup G.
 Proof.
   rapply (Build_Subgroup' (fun x => x = mon_unit)).
   1: reflexivity.
@@ -205,7 +205,7 @@ Proof.
 Defined.
 
 (** Every group is a (maximal) subgroup of itself *)
-Definition maximal_subgroup {G} : Subgroup G.
+Definition maximal_subgroup G : Subgroup G.
 Proof.
   rapply (Build_Subgroup G (fun x => Unit)).
   split; auto; exact _.
@@ -477,7 +477,7 @@ Defined.
 
 (** The property of being the trivial subgroup is useful. *)
 Definition IsTrivialSubgroup {G : Group} (H : Subgroup G) : Type :=
-  forall x, H x <-> trivial_subgroup x.
+  forall x, H x <-> trivial_subgroup G x.
 Existing Class IsTrivialSubgroup.
 
 Global Instance istrivialsubgroup_trivial_subgroup {G : Group}

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
@@ -143,7 +143,7 @@ End IdealElements.
 
 (** The trivial subgroup is a left ideal. *)
 Global Instance isleftideal_trivial_subgroup (R : Ring)
-  : IsLeftIdeal (R := R) trivial_subgroup.
+  : IsLeftIdeal (trivial_subgroup R).
 Proof.
   intros r x p.
   rhs_V nrapply (rng_mult_zero_r).
@@ -152,12 +152,12 @@ Defined.
 
 (** The trivial subgroup is a right ideal. *)
 Global Instance isrightideal_trivial_subgroup (R : Ring)
-  : IsRightIdeal (R := R) trivial_subgroup
+  : IsRightIdeal (trivial_subgroup R)
   := isleftideal_trivial_subgroup _.
 
 (** The trivial subgroup is an ideal. *)
 Global Instance isideal_trivial_subgroup (R : Ring)
-  : IsIdeal (R := R) trivial_subgroup
+  : IsIdeal (trivial_subgroup R)
   := {}.
 
 (** We call the trivial subgroup the "zero ideal". *)
@@ -167,17 +167,17 @@ Definition ideal_zero (R : Ring) : Ideal R := Build_Ideal R _ _.
 
 (** The maximal subgroup is a left ideal. *)
 Global Instance isleftideal_maximal_subgroup (R : Ring)
-  : IsLeftIdeal (R := R) maximal_subgroup
+  : IsLeftIdeal (maximal_subgroup R)
   := ltac:(done).
 
 (** The maximal subgroup is a right ideal. *)
 Global Instance isrightideal_maximal_subgroup (R : Ring)
-  : IsRightIdeal (R := R) maximal_subgroup
+  : IsRightIdeal (maximal_subgroup R)
   := isleftideal_maximal_subgroup _.
 
 (** The maximal subgroup is an ideal.  *)
 Global Instance isideal_maximal_subgroup (R : Ring)
-  : IsIdeal (R:=R) maximal_subgroup
+  : IsIdeal (maximal_subgroup R)
   := {}.
 
 (** We call the maximal subgroup the "unit ideal". *)