Skip to content

Simplification of galois_misom and galois_isog #105

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

Open
CohenCyril wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Simplification of galois_misom and galois_isog #105

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
10 changes: 5 additions & 5 deletions theories/xmathcomp/map_gal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_fingroup all_algebra.

Check warning on line 2 in theories/xmathcomp/map_gal.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20) 

Notations "\pi ( _ )" defined at level 2 and "\pi"

Check warning on line 2 in theories/xmathcomp/map_gal.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.20) 

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
From mathcomp Require Import all_solvable all_field.
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
From Abel Require Import various char0.
Expand Down Expand Up @@ -193,7 +193,7 @@
Qed.

Lemma galois_misom (k K F : {subfield L})
(H := 'Gal((K * F) / F)%g) (H' := 'Gal (K / (K :&: F))%g) :
(H := 'Gal((K * F) / F)%g) (H' := 'Gal (K / F)%g) :
galois k K -> (k <= F)%VS -> misom H H' (normalField_cast K).
Proof.
move=> gal_kK kF; have kK := galois_subW gal_kK.
Expand All @@ -214,7 +214,8 @@
have /eqP/gal_eqP/(_ _ xiK) := mker ker_u.
rewrite /normalField_cast galK ?KF// => ->; rewrite gal_id.
by rewrite (fixed_gal _ Hu)// field_subvMl.
apply/eqP; rewrite eq_sym galois_eq ?(capv_galois kF gal_kK)//.
apply/esym/eqP; rewrite [X in X == _]gal_cap capvC.
rewrite galois_eq ?(capv_galois kF gal_kK)//.
rewrite eqEsubv; apply/andP; split; apply/subvP => x; last first.
rewrite memv_cap => /andP[Kx Fx].
apply/fixedFieldP => // _ /morphimP[/= v Hv _ ->].
Expand All @@ -228,7 +229,7 @@
Qed.

Lemma galois_isog (k K F : {subfield L}) : galois k K -> (k <= F)%VS ->
'Gal((K * F) / F) \isog 'Gal (K / K :&: F).
'Gal((K * F) / F) \isog 'Gal (K / F).
Proof. by move=> galkK /(galois_misom galkK) /misom_isog. Qed.

Lemma subv_big_prodv_seq I r (P : {pred I}) (k : {subfield L})
Expand Down Expand Up @@ -794,8 +795,7 @@
rewrite (@galois_prodvr _ _ k) ?normalClosure_galois//.
rewrite ?prodvSl ?sub_normalClosure//=.
rewrite (isog_sol (galois_isog (normalClosure_galois _) _))//.
rewrite (solvableS _ solkE)// galS// subv_cap kF.
by rewrite galois_subW ?normalClosure_galois.
by rewrite (solvableS _ solkE)// galS//.
Qed.

Import AEnd_FinGroup.
Expand Down
Loading