Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added definition for cyclic' to AbGroups/Cyclic.v #2050

Merged
merged 4 commits into from
Aug 6, 2024
Merged

Added definition for cyclic' to AbGroups/Cyclic.v #2050

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
55adc5b
Added definition for cyclic' to AbGroups/Cyclic.v
ndcroos Aug 6, 2024
5d59e74
Comment, newline and grp_image change
ndcroos Aug 6, 2024
a6c4ec7
Removing universe variables
ndcroos Aug 6, 2024
db5f035
Removing universe variables, now builds
ndcroos Aug 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 5 additions & 3 deletions theories/Algebra/AbGroups/Cyclic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,8 +77,10 @@ Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z

(** The [n]-th cyclic group is the cokernel of [Z1_mul_nat n]. *)
Definition cyclic@{u v | u < v} `{Funext} (n : nat) : AbGroup@{u}
:= ab_cokernel@{u v} (Z1_mul_nat n).
:= ab_cokernel@{u} (Z1_mul_nat n).

(** ** Alternative definition of cyclic group *)

(** The [n]-th cyclic group is the cokernel of [ab_mul n]. *)
Definition cyclic'@{u v | u < v} `{Funext} (n : nat) : AbGroup@{u}
:= ab_cokernel@{u v} (ab_mul (A:=abgroup_Z) n).
Definition cyclic'@{u} (n : nat) : AbGroup@{u}
:= ab_cokernel@{u} (ab_mul (A:=abgroup_Z) n).
2 changes: 1 addition & 1 deletion theories/Algebra/AbSES/SixTerm.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ Defined.
(** The main result of this section. *)
Theorem ext_cyclic_ab@{u v w | u < v, v < w} `{Univalence}
Alizter marked this conversation as resolved.
Show resolved Hide resolved
(n : nat) `{emb : IsEmbedding (Z1_mul_nat n)} {A : AbGroup@{u}}
: ab_cokernel@{v w} (ab_mul (A:=A) n)
: ab_cokernel@{v} (ab_mul (A:=A) n)
$<~> ab_ext@{u v} (cyclic'@{u v} n) A.
(* We take a large cokernel in order to apply [abses_cokernel_iso]. *)
Proof.
Expand Down
2 changes: 1 addition & 1 deletion theories/Algebra/Groups/Image.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Local Open Scope mc_scope.
Local Open Scope mc_mult_scope.

(** The image of a group homomorphism between groups is a subgroup *)
Definition grp_image {A B : Group} (f : A $-> B) : Subgroup B.
Definition grp_image {A B : Group} (f : GroupHomomorphism A B) : Subgroup B.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why was this changed? It gets rid of one universe variable, but we don't generally try to avoid wild category notation just for that. (Moreover, I think with the next release of Coq those stray universe variables might go away.)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was my suggestion from earlier, and yes, this will go away when Coq gets algebraic universes. I don't know if it will be the next release of Coq however. It still seems unfinished.

FTR @ndcroos the issue here is that the wildcat of groups should land in the unvierse Set+1 however Coq doesn't let you write that for the moment, meaning we have to introduce a new universe variable strictly larger.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, I missed that comment. But it seems weird to optimize that one result in Image.v to save a universe variable, but not the other results. And it's really orthogonal to this PR.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One difference here is that we are expecting no universe variables, whereas in other places it is one extra. Anyway, we can cleanup other universe issues some other time.

Proof.
snrapply (Build_Subgroup' (fun b => hexists (fun a => f a = b))).
- exact _.
Expand Down
Loading