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

Elimination principles for GroupCoeq #2184

Merged
merged 12 commits into from
Mar 16, 2025
+174 −93
Merged

Elimination principles for GroupCoeq #2184

Changes from 1 commit
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
d7356e9
constructors and functoriality for GroupCoeq
Alizter Dec 29, 2024
d159e72
replace ugly change with explicit wildcat term
Alizter Jan 7, 2025
bd5c53b
Groups/FreeProduct: use $-> to simplify later goals; change WildCat i…
jdchristensen Feb 17, 2025
ebb73ff
GroupCoeq: slightly simplify one proof
jdchristensen Feb 17, 2025
9193956
FreeProduct: change Global Instances to Local
jdchristensen Feb 18, 2025
2e82f42
add comment about unifying equiv_groupcoeq_rec
Alizter Feb 24, 2025
dc15a84
add comment about complicated wildcat term
Alizter Feb 24, 2025
d0c7d05
improve proof of equiv_groupcoeq_rec
Alizter Feb 24, 2025
8b63aec
FreeProduct, GroupCoeq: speed up/simplify some proofs
jdchristensen Mar 13, 2025
dd823b0
Move FreeProduct_rec after FreeProduct_ind*
jdchristensen Mar 13, 2025
7fdcbaf
FreeProduct: split Section for speed and improve implicit arguments
jdchristensen Mar 15, 2025
43e5cd4
FreeProduct, GroupCoeq: fix nrapply warnings
jdchristensen Mar 15, 2025
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
Prev Previous commit
Next Next commit
FreeProduct: change Global Instances to Local
  • Loading branch information
@jdchristensen
jdchristensen committed Mar 15, 2025
commit 9193956edbb7d0f070a3681d828e41caff61e342
18 changes: 9 additions & 9 deletions theories/Algebra/Groups/FreeProduct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,7 +273,7 @@ Section FreeProduct.
(** Now for the group structure *)

(** The group operation is concatenation of the underlying list. Most of the work is spent showing that it respects the path constructors. *)
#[export] Instance sgop_amal_type : SgOp amal_type.
Local Instance sgop_amal_type : SgOp amal_type.
Proof.
intros x y; revert x.
srapply amal_type_rec; intros x; revert y.
Expand Down Expand Up @@ -350,12 +350,12 @@ Section FreeProduct.
Defined.

(** The identity element is the empty list *)
#[export] Instance monunit_amal_type : MonUnit amal_type.
Local Instance monunit_amal_type : MonUnit amal_type.
Proof.
exact (amal_eta nil).
Defined.

#[export] Instance inverse_amal_type : Inverse amal_type.
Local Instance inverse_amal_type : Inverse amal_type.
Proof.
srapply amal_type_rec.
{ intros w.
Expand Down Expand Up @@ -420,7 +420,7 @@ Section FreeProduct.
apply amal_omega_K. }
Defined.

#[export] Instance associative_sgop_m : Associative sg_op.
Local Instance associative_sgop_m : Associative sg_op.
Proof.
intros x y.
rapply amal_type_ind_hprop; intro z; revert y.
Expand All @@ -430,13 +430,13 @@ Section FreeProduct.
rapply app_assoc.
Defined.

#[export] Instance leftidentity_sgop_amal_type : LeftIdentity sg_op mon_unit.
Local Instance leftidentity_sgop_amal_type : LeftIdentity sg_op mon_unit.
Proof.
rapply amal_type_ind_hprop; intro x.
reflexivity.
Defined.

#[export] Instance rightidentity_sgop_amal_type : RightIdentity sg_op mon_unit.
Local Instance rightidentity_sgop_amal_type : RightIdentity sg_op mon_unit.
Proof.
rapply amal_type_ind_hprop; intro x.
napply (ap amal_eta).
Expand Down Expand Up @@ -505,13 +505,13 @@ Section FreeProduct.
apply amal_omega_K.
Defined.

#[export] Instance leftinverse_sgop_amal_type : LeftInverse (.*.) (^) mon_unit.
Local Instance leftinverse_sgop_amal_type : LeftInverse (.*.) (^) mon_unit.
Proof.
rapply amal_type_ind_hprop; intro x.
apply amal_eta_word_concat_Vw.
Defined.

#[export] Instance rightinverse_sgop_amal_type : RightInverse (.*.) (^) mon_unit.
Local Instance rightinverse_sgop_amal_type : RightInverse (.*.) (^) mon_unit.
Proof.
rapply amal_type_ind_hprop; intro x.
apply amal_eta_word_concat_wV.
Expand Down Expand Up @@ -564,7 +564,7 @@ Section FreeProduct.
rapply left_identity. }
Defined.

#[export] Instance issemigrouppreserving_AmalgamatedFreeProduct_rec'
Local Instance issemigrouppreserving_AmalgamatedFreeProduct_rec'
(X : Group) (h : GroupHomomorphism H X) (k : GroupHomomorphism K X)
(p : h o f == k o g)
: IsSemiGroupPreserving (AmalgamatedFreeProduct_rec' X h k p).
Expand Down