(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype tuple div.
From mathcomp
Require Import bigop prime finset fingroup ssralg finalg zmodp abelian.
From mathcomp
Require Import matrix vector falgebra finfield action poly ssrint cyclotomic.
From mathcomp
Require Import fieldext mxalgebra mxpoly.

(************************************************************************************************)
(*   Basic algebraic number theory concepts from Milne, J.S.: Algebraic Number Theory.          *)
(*   We work in the setting of an extension field L0 : fieldextType F. At this point,           *)
(*   an integral domain is represented as a collective predicate on L0 closed under             *) 
(*   subring operations. A module over the integral domain A is represented as a                *)
(*   Prop-valued predicate closed under the operations (0, x + y, x - y, x * y). It             *)
(*   is not a-priori made a collective predicate since we first need to establish the           *)
(*   Basis Lemma in order to show decidability.                                                 *)
(*                                                                                              *)
(*         integral A l <-> l is integral over the domain A, i.e., it satisfies a polynomial    *)
(*                          over A. This is currently a Prop-valued predicate since we          *)
(*                          quantify over all polynomials over A. An alternative definition     *)
(*                          would be to say that the minimal polynomial of l over the field     *)
(*                          of fractions of A is itself a polynomial over A. The latter is      *)
(*                          a decidable property and the equivalence of the two definitions     *)
(*                          is provided by Prop. 2.11 in Milne.                                 *) 
(*         int_closed A <-> A is integrally closed.                                             *)
(*       int_closure A L == The integral closure of A in L. This is currently a Prop-valued     *)
(*                          predicate.                                                          *) 
(*    is_frac_field A K <-> K is the field of fractions of A. The condition of every k \in K    *)
(*                          arising as a quotient a / b for a,b \in K is skolemized. This is    *)
(*                          not strictly necessary since L0 has a canonical choiceType          *)
(*                          structure but it facilitates some of the later proofs.              *) 
(*  frac_field_alg_int A == Every element l arises as a quotient b / a, where a is in A and b   *)
(*                          is integral over A. The statement of the theorem is skolemized,     *)
(*                          which is not strictly necessary.                                    *) 
(*       int_clos_incl A == Every element of A is integral over A.                              *)
(*  int_subring_closed A == The integral closure of A is closed under the subring operations    *)
(*                          (a - b, a * b). The proof of this lemma uses an equivalent          *)
(*                          characterization of integrality, cf. Prop. 2.4 in Milne, which is   *)
(*                          captured by the Lemmas intPl and intPr. The former states that      *)
(*                          if there exists a nonzero finitely-generated A-module closed under  *)
(*                          multiplication by l, then l is integral over A. The latter states   *)
(*                          that if l is integral over A, then the A-algebra generated by l is  *)
(*                          closed under multiplication by l. Note: These lemmas probably need  *)
(*                          better names.                                                       *)         
(*     int_zmod_closed A == The integral closure of A is closed under subtraction.              *)
(*     int_mulr_closed A == The integral closure of A is closed under multiplication.           *)
(*              tr L l k == The trace of l * k on L; the result is in the field of scalars F.   *)          
(*                          The function tr is scalar in its first argument.                    *)
(*                tr_sym == The trace function is commutative.                                  *)
(*             ndeg Q V <-> The binary function Q : vT -> vT -> rT is nondegenerate on the      *)
(*                          subspace V.                                                         *) 
(*        dual_basis U X == The dual basis of U for X, with respect to the trace bilinear form. *)
(*               trK K L == The trace function on L viewed as a subfield over K.                *)
(*         trK_int A K L == If k and l are integral over A then their trace is in A, provided   *)
(*                          A is an integrally closed domain, K is its field of fractions, and  *)
(*                          L extends K.                                                        *)
(*           module A M <-> M is an A-module.                                                   *)
(*          span_mod A X == The A-module generated by X.                                        *)
(*         submod A M N <-> M is a submodule of N over A.                                       *)
(*   basis_of_mod A M X <-> X is the basis of the A-module M.                                   *)
(*            ideal A N <-> N is an A-ideal.                                                    *)   
(*                PID A <-> Every ideal in A is principal.                                      *)  
(*    int_mod_closed A L == The integral closure of A in L is an A-module.                      *)
(*   basis_lemma I Ifr K == The integral closure of I in K is a free module, provided I is an   *)
(*                          integrally-closed principal ideal domain contained in K, Ifr is the *)
(*                          field of fractions of I, and the trace function trK Ifr K is        *)
(*                          nondegenerate on K.                                                 *)
(************************************************************************************************)

Import GRing.Theory.
Import DefaultKeying GRing.DefaultPred.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope ring_scope.

Section Integral.

Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (K L : {subfield L0}).

Hypothesis Asubr : subring_closed A.

Definition integral l := exists p, [/\ p \is monic, p \is a polyOver A & root p l].
Definition int_closed := {in A, forall a b, integral (a / b) -> (a / b) \in A}.
Definition int_closure l := l \in L /\ integral l.
Definition is_frac_field := {subset A <= K} /\ exists f, forall k, f k != 0 /\
  (k \in K -> f k \in A /\ f k * k \in A).

Hypothesis AfracK : is_frac_field.

Lemma frac_field_alg_int : exists f, forall l, [/\ f l != 0, f l \in A & integral (f l * l)].
Proof.
have [Aid _ Amcl] := Asubr; have Amulr : mulr_closed A := Asubr.
have [AsubK [f /all_and2-[fH0 /(_ _)/all_and2-/all_and2-[fHa fHk]]]] := AfracK.
pose g := fun l => let p := minPoly K l in \prod_(i < size p) f p`_i; exists g => l.
pose p := minPoly K l; pose n := (size p).-1.
pose s := mkseq (fun i => p`_i * (g l) ^+ (n - i)%N) (size p).
have kI (i : 'I_(size p)) : p`_i \in K by apply/all_nthP => //; apply/minPolyOver.
have glA : g l \in A by rewrite/g; elim/big_ind: _ => // i _; apply/fHa.
have pmon: p`_n = 1 by have /monicP := monic_minPoly K l.
have an1: nth 0 s n = 1 by rewrite /n nth_mkseq ?pmon ?mul1r ?subnn ?size_minPoly. 
have eqPs: (Poly s) = s :> seq L0.
  by rewrite (PolyK (c := 0)) // -nth_last size_mkseq an1 oner_neq0.
have ilen i : i < size p -> i <= n by move => iB; rewrite /n -ltnS prednK // size_minPoly.
split => //; first by apply/prodf_neq0 => i _.
exists (Poly s); split; last first; last by rewrite monicE lead_coefE eqPs // size_mkseq an1.
  rewrite /root -(mulr0 ((g l) ^+ n)); have <- := minPolyxx K l.
  rewrite !horner_coef eqPs size_mkseq big_distrr; apply/eqP/eq_bigr => i _.
  rewrite nth_mkseq // exprMn //=; rewrite !mulrA; congr (_ * _); rewrite -mulrA mulrC.
  by congr (_ * _); rewrite -exprD subnK ?ilen.
apply/(all_nthP 0) => i; rewrite eqPs size_mkseq => iB; rewrite nth_mkseq //.
  have := ilen _ iB; rewrite leq_eqVlt => /orP.
  case; first by move /eqP ->; rewrite subnn pmon mulr1.
  rewrite -subn_gt0 => {pmon ilen eqPs an1} /prednK <-; rewrite exprS mulrA /= Amcl ?rpredX //.
  rewrite /g (bigD1 (Ordinal iB)) //= mulrA; apply/Amcl.
    by rewrite mulrC; apply/fHk/(kI (Ordinal iB)).
  by rewrite rpred_prod => // j _; apply/fHa. 
Qed.

Lemma int_clos_incl a : a \in A -> integral a.
Proof.
move=> ainA; exists ('X - a%:P); rewrite monicXsubC root_XsubC.
rewrite polyOverXsubC => //; by apply Asubr.
Qed.

Lemma intPl (I : eqType) G (r : seq I) l : has (fun x => G x != 0) r ->
  (forall e, e \in r -> {f | \sum_(e' <- r) f e' * G e' = l * G e & forall e', f e' \in A}) ->
  integral l.
Proof.
have Aaddr : addr_closed A := Asubr; have Amulr : mulr_closed A := Asubr.
have Aoppr : oppr_closed A := Asubr; have [Aid _ _] := Asubr.
move => rn gen; pose s := in_tuple r; pose g j := gen (tnth s j) (mem_tnth j s).
pose f j := sval (g j); pose fH j := svalP (g j).
pose M := \matrix_(i, j < size r) f j (tnth s i).
exists (char_poly M); rewrite char_poly_monic; split => //.
  apply/rpred_sum => p _; apply/rpredM; first by apply/rpredX; rewrite rpredN polyOverC.
  apply/rpred_prod => i _; rewrite !mxE /= rpredB ?rpredMn ?polyOverX ?polyOverC ?/f //.
  by have [_ fH2] := fH (perm.PermDef.fun_of_perm p i).
rewrite -eigenvalue_root_char; apply/eigenvalueP; move: rn => /hasP[x] /(nthP x)[k kB <- xn].
exists (\row_(i < size r) G (tnth s i)); last first.
  move: xn; apply/contra => /eqP/matrixP-v0; have := v0 0 (Ordinal kB).
  by rewrite !mxE (tnth_nth x) => <-.
rewrite -rowP => j; rewrite !mxE; have [fH1 _] := fH j; rewrite -fH1 (big_nth x) big_mkord.
by apply/eq_bigr => /= i _; rewrite /M !mxE (tnth_nth x) mulrC.
Qed.

Lemma intPr l : integral l -> exists r : seq L0,
  [/\ r != nil, all A r & \sum_(i < size r) r`_i * l ^+ i = l ^+ (size r)].
Proof.
move => [p [pm pA pr]]; pose n := size p; pose r := take n.-1 (- p).
have ps : n > 1.
  rewrite ltnNge; apply/negP => /size1_polyC pc; rewrite pc in pr pm => {pc}.
  move: pr => /rootP; rewrite hornerC => pc0.
  by move: pm; rewrite monicE lead_coefC pc0 eq_sym oner_eq0.
have rs : size r = n.-1 by rewrite /r size_takel // size_opp leq_pred.
exists r; split.
  apply/eqP => /nilP; rewrite /nilp /r size_takel; last by rewrite size_opp leq_pred.
  by rewrite -subn1 subn_eq0 leqNgt ps.
  have : - p \is a polyOver A by rewrite rpredN //; apply Asubr.
  by move => /allP-popA; apply/allP => x /mem_take /popA.
move: pr => /rootP; rewrite horner_coef -(prednK (n := size p)); last by rewrite ltnW.
rewrite big_ord_recr /= rs; have := monicP pm; rewrite /lead_coef => ->; rewrite mul1r => /eqP.
rewrite addrC addr_eq0 -sumrN => /eqP => ->; apply/eq_bigr => i _; rewrite /r nth_take //.    
by rewrite coefN mulNr.
Qed.

Lemma int_subring_closed a b : integral a -> integral b ->
  integral (a - b) /\ integral (a * b).
Proof.
have [A0 _ ] := (Asubr : zmod_closed A); have [A1 Asubr2 Amulr2] := Asubr.
move => /intPr[ra [/negbTE-ran raA raS]] /intPr[rb [/negbTE-rbn rbA rbS]].
pose n := size ra; pose m := size rb; pose r := Finite.enum [finType of 'I_n * 'I_m].
pose G (z : 'I_n * 'I_m) := let (k, l) := z in a ^ k * b ^l.
have [nz mz] : 0 < n /\ 0 < m.
  by rewrite !lt0n; split; apply/negP; move => /nilP/eqP; rewrite ?ran ?rbn.
have rnn : has (fun x => G x != 0) r.
  apply/hasP; exists (Ordinal nz, Ordinal mz); first by rewrite /r -enumT mem_enum.
  by rewrite /G mulr1 oner_neq0.
pose h s i : 'I_(size s) -> L0 := fun k => if (i != size s) then (i == k)%:R else s`_k.
pose f i j (z : 'I_n * 'I_m) : L0 := let (k, l) := z in h ra i k * h rb j l.
have fA i j : forall z, f i j z \in A.
  have hA s k l : all A s -> h s k l \in A.
    move => /allP-sa; rewrite /h; case (eqVneq k (size s)) => [/eqP ->|->].
      by apply/sa/mem_nth. 
    by case (eqVneq k l) => [/eqP ->|/negbTE ->].
  by move => [k l]; rewrite /f; apply/Amulr2; apply/hA.
have fS i j : (i <= n) -> (j <= m) -> \sum_(z <- r) f i j z * G z = a ^ i * b ^ j.
  have hS s k c : (k <= size s) -> \sum_(l < size s) s`_l * c ^ l = c ^ (size s) ->
    \sum_(l < size s) h s k l * c ^ l = c ^ k.
    move => kB sS; rewrite /h; case (eqVneq k (size s)) => [->|kn {sS}]; first by rewrite eqxx.
    rewrite kn; rewrite leq_eqVlt (negbTE kn) /= in kB => {kn}.
    rewrite (bigD1 (Ordinal kB)) //= eqxx mul1r /= -[RHS]addr0; congr (_ + _).
    by apply/big1 => l; rewrite eq_sym => kl; have : k != l := kl => /negbTE ->; rewrite mul0r.
  move => iB jB; rewrite -(hS ra i a) // -(hS rb j b) // mulr_suml.
  rewrite (eq_bigr (fun k => \sum_(l < m) (h ra i k * a ^ k) * (h rb j l * b ^ l))).
    rewrite pair_bigA; apply eq_bigr => [[k l] _]; rewrite !mulrA; congr (_ * _).
    by rewrite -!mulrA [in h rb j l * a ^ k] mulrC.
  by move => k _; rewrite mulr_sumr.
pose fB i j z := f i.+1 j z - f i j.+1 z; pose fM i j z := f i.+1 j.+1 z.
have fBA i j z : fB i j z \in A by rewrite /fB Asubr2.
have fBM i j z : fM i j z \in A by rewrite /fM.
split; apply/(@intPl _ G r) => //= [[i j] _]; [exists (fB i j) | exists (fM i j)] => //.
  rewrite /fB [in RHS]/G mulrBl mulrA -exprS [in b * (a ^ i * b ^ j)] mulrC -mulrA -exprSr.
  rewrite -(fS _ _ (ltnW (ltn_ord i))) // -(fS _ _ _ (ltnW (ltn_ord j))) //.
  by rewrite -sumrB; apply/eq_bigr => [[k l] _]; apply/mulrBl.
by rewrite /fM [in RHS]/G mulrA [in (a * b) * a ^ i] mulrC mulrA -exprSr -mulrA -exprS -!fS.
Qed.

Lemma int_zmod_closed a b : integral a -> integral b -> integral (a - b).
Proof. by move => aI bI; have [Azmod] := int_subring_closed aI bI. Qed.

Lemma int_mulr_closed a b : integral a -> integral b -> integral (a * b).
Proof. by move => aI bI; have [_] := int_subring_closed aI bI. Qed.

End Integral.

Section Trace.

Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield L0}).

Implicit Types k l : L0.

Definition tr : L0 -> L0 -> F := fun l k =>
  let X := vbasis L in
    let M := \matrix_(i, j) coord X i (l * k * X`_j)
      in \tr M.

Fact tr_is_scalar l : scalar (tr l).
Proof.
move => c a b; rewrite /tr  -!linearP /=; congr (\tr _); apply/matrixP => i j; rewrite !mxE.
by rewrite mulrDr mulrDl linearD /= -scalerAr -scalerAl linearZ.
Qed.

Canonical tr_additive l := Additive (@tr_is_scalar l).
Canonical tr_linear l := AddLinear (@tr_is_scalar l).
  
Lemma tr_sym : commutative tr.
Proof. by move => a b; rewrite /tr mulrC. Qed.

Hypothesis Asubr : subring_closed A.
Hypothesis Aint  : int_closed A.
Hypothesis Afrac : is_frac_field A 1%AS.

Lemma tr_int k l : integral A k -> integral A l -> (tr k l)%:A \in A.
Proof. admit. Qed.

Section NDeg.

Variable (vT : vectType F) (rT : ringType) (Q : vT -> vT -> rT) (V : {vspace vT}).

Definition ndeg := forall (l : vT), l != 0 -> l \in V -> exists (k : vT), k \in V /\ Q l k != 0.

End NDeg.

Variable (U : {vspace L0}).
Let m := \dim U.
Variable (X : m.-tuple L0).

Lemma dual_basis_def :
  {Y : m.-tuple L0 | ndeg tr U -> basis_of U X -> basis_of U Y /\
  forall (i : 'I_m), tr X`_i Y`_i = 1 /\
  forall (j : 'I_m), j != i -> tr X`_i Y`_j = 0}.
Proof.
pose Uv := subvs_vectType U; pose Fv := subvs_FalgType (1%AS : {aspace L0}); 
pose HomV := [vectType _ of 'Hom(Uv, Fv)].
pose tr_sub : Uv -> Uv -> Fv := fun u v => (tr (vsval u) (vsval v))%:A.
have HomVdim : \dim {:HomV} = m by rewrite dimvf /Vector.dim /= /Vector.dim /= dimv1 muln1.
have [f fH] : {f : 'Hom(Uv, HomV) | forall u, f u =1 tr_sub u}.
  have lf1 u : linear (tr_sub u) by move => c x y; rewrite /tr_sub linearP scalerDl scalerA.
  have lf2 : linear (fun u => linfun (Linear (lf1 u))).
    move => c x y; rewrite -lfunP => v; rewrite add_lfunE scale_lfunE !lfunE /= /tr_sub.
    by rewrite tr_sym linearP scalerDl scalerA /=; congr (_ + _); rewrite tr_sym.
  by exists (linfun (Linear lf2)) => u v; rewrite !lfunE.
have [Xdual XdualH] : {Xdual : m.-tuple HomV |
  forall (i : 'I_m) u, Xdual`_i u = (coord X i (vsval u))%:A}.
  have lg (i : 'I_m) : linear (fun u : Uv => (coord X i (vsval u))%:A : Fv).
    by move => c x y; rewrite linearP /= scalerDl scalerA.
  exists (mktuple (fun i => linfun (Linear (lg i)))) => i u.
  by rewrite -tnth_nth tnth_mktuple !lfunE.
have [finv finvH] : {finv : 'Hom(HomV, L0) | finv =1 vsval \o (f^-1)%VF}.
  by exists (linfun vsval \o f^-1)%VF => u; rewrite comp_lfunE lfunE. 
pose Y := map_tuple finv Xdual; exists Y => Und Xb.
have Ydef (i : 'I_m) : Y`_i = finv Xdual`_i by rewrite -!tnth_nth tnth_map.
have XiU (i : 'I_m) : X`_i \in U by apply/(basis_mem Xb)/mem_nth; rewrite size_tuple.
have Xii (i : 'I_m) : coord X i X`_i = 1%:R.
  by rewrite coord_free ?eqxx //; apply (basis_free Xb).
have Xij (i j : 'I_m) : j != i -> coord X i X`_j = 0%:R.
  by rewrite coord_free; [move => /negbTE -> | apply (basis_free Xb)].
have Xdualb : basis_of fullv Xdual.
  suffices Xdualf : free Xdual.
    rewrite /basis_of Xdualf andbC /= -dimv_leqif_eq ?subvf // eq_sym HomVdim.
    by move: Xdualf; rewrite /free => /eqP => ->; rewrite size_tuple.
  apply/freeP => k sX i.  
  suffices: (\sum_(i < m) k i *: Xdual`_i) (vsproj U X`_i) = (k i)%:A.
    by rewrite sX zero_lfunE => /esym /eqP; rewrite scaler_eq0 oner_eq0 orbF => /eqP.
  rewrite sum_lfunE (bigD1 i) //= scale_lfunE XdualH vsprojK // Xii.
  rewrite scaler_nat -[RHS]addr0; congr (_ + _); apply/big1 => j; rewrite eq_sym => ineqj.
  by rewrite scale_lfunE XdualH vsprojK ?Xij // scaler_nat scaler0.
have finj : (lker f = 0)%VS.
  apply/eqP; rewrite -subv0; apply/subvP=> u; rewrite memv_ker memv0 => /eqP-f0.
  apply/contraT => un0; have {un0} [k [kiU /negP[]]] := Und (vsval u) un0 (subvsP u).
  have /eqP := fH u (vsproj U k).
  by rewrite /tr_sub vsprojK // f0 zero_lfunE eq_sym scaler_eq0 oner_eq0 orbF.
have flimg : limg f = fullv.
  apply/eqP; rewrite -dimv_leqif_eq ?subvf // limg_dim_eq; last by rewrite finj capv0.
  by rewrite HomVdim dimvf /Vector.dim.
have finvK : cancel finv (f \o vsproj U).
  by move => u; rewrite finvH /= vsvalK; apply/limg_lfunVK; rewrite flimg memvf.
have finv_inj : (lker finv = 0)%VS by apply/eqP/lker0P/(can_inj finvK).
have finv_limg : limg finv = U. 
  apply/eqP; rewrite -dimv_leqif_eq; first by rewrite limg_dim_eq ?HomVdim ?finv_inj ?capv0.   
  by apply/subvP => u /memv_imgP [h _] ->; rewrite finvH subvsP.
have Xt (i j : 'I_m) : (f \o vsproj U) Y`_j (vsproj U X`_i) = (tr Y`_j X`_i)%:A.
  by rewrite fH /tr_sub !vsprojK // Ydef finvH subvsP.
have Xd (i j : 'I_m) : (f \o vsproj U) Y`_j (vsproj U X`_i) = Xdual`_j (vsproj U X`_i).
  by rewrite Ydef finvK.
have Ainj := fmorph_inj [rmorphism of in_alg Fv].
split => [| i]; first by rewrite -{1}finv_limg limg_basis_of // capfv finv_inj.
split => [| j]; first by have := Xt i i; rewrite tr_sym Xd XdualH vsprojK // Xii => /Ainj.
by rewrite eq_sym => inj; have := Xt i j; rewrite tr_sym Xd XdualH vsprojK // Xij // => /Ainj.
Qed.

Definition dual_basis : m.-tuple L0 := sval dual_basis_def.

Hypothesis Und : ndeg tr U.
Hypothesis Xb : basis_of U X.

Lemma dualb_basis : basis_of U dual_basis.
Proof. by have [Yb _] := svalP dual_basis_def Und Xb; apply Yb. Qed.

Lemma dualb_orth :
  forall (i : 'I_m), tr X`_i dual_basis`_i = 1 /\
  forall (j : 'I_m), j != i -> tr X`_i dual_basis`_j = 0.
Proof. by have [_] := svalP dual_basis_def Und Xb. Qed.

End Trace.

Section TraceFieldOver.

Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (K L : {subfield L0}).

Implicit Types k l : L0.

Let K' := subvs_fieldType K.
Let L0' := fieldOver_fieldExtType K.

Definition trK : L0 -> L0 -> K' := tr (aspaceOver K L).
 
Lemma trK_ndeg (U : {aspace L0}) : (K <= U)%VS ->
  (ndeg trK U <-> ndeg (tr (aspaceOver K L)) (aspaceOver K U)).
Proof.
move => UsubL; have UU' : aspaceOver K U =i U := mem_aspaceOver UsubL.
split => [ndK l lnz | nd l lnz].
  by rewrite UU' => liU; have [k] := ndK l lnz liU; exists k; rewrite UU'.
by rewrite -UU' => liU'; have [k] := nd l lnz liU'; exists k; rewrite -UU'.
Qed.

Hypothesis Asubr : subring_closed A.
Hypothesis Aint  : int_closed A.
Hypothesis Afrac : is_frac_field A K.
Hypothesis AsubL : {subset A <= L}.

Lemma trK_int k l : integral A k -> integral A l -> ((trK k l)%:A : L0') \in A.
Proof. admit. Qed.

End TraceFieldOver.

Section BasisLemma.

Section Modules.

Variable (F : fieldType) (L0 : fieldExtType F) (A : pred L0).

Implicit Types M N : L0 -> Prop.

Definition module M := M 0 /\ forall a k l, a \in A -> M k -> M l -> M (a * k - l).
Definition span_mod X m := exists2 r : (size X).-tuple L0,
  all A r & m = \sum_(i < size X) r`_i * X`_i.
Definition submod M N := forall m, M m -> N m.
Definition basis_of_mod M X := free X /\ submod M (span_mod X) /\ forall m, m \in X -> M m.
Definition ideal N := submod N A /\ module N.
Definition PID := forall (N : L0 -> Prop), ideal N ->
  exists2 a, N a & forall v, N v -> exists2 d, d \in A & d * a = v.

Variable L : {subfield L0}.

Hypothesis Asubr : subring_closed A.
Hypothesis AsubL : {subset A <= L}.

Lemma int_mod_closed : module (int_closure A L).
Proof.
have [A0 _] : zmod_closed A := Asubr; split.
  by rewrite /int_closure mem0v; split => //; apply/int_clos_incl.
move => a k l aA [kI kL] [lI lL]; split; first by rewrite rpredB ?rpredM //; apply/AsubL.
by apply/int_zmod_closed => //; apply/int_mulr_closed => //; apply/int_clos_incl. 
Qed.

End Modules.

Variable (F0 : fieldType) (E : fieldExtType F0) (I : pred E) (Ifr K : {subfield E}).

Hypothesis Isubr : subring_closed I.
Hypothesis Iint : int_closed I.
Hypothesis Ipid : PID I.
Hypothesis Ifrac : is_frac_field I Ifr. 
Hypothesis IsubK : {subset I <= K}.
Hypothesis Knd :  ndeg (trK Ifr K) K.

Lemma basis_lemma : exists X : (\dim_Ifr K).-tuple E, basis_of_mod I (int_closure I K) X.
Proof.
suffices FisK (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield L0}) :
  subring_closed A -> int_closed A -> PID A -> is_frac_field A 1 -> ndeg (tr L) L ->
  exists2 X, size X == \dim L & basis_of_mod A (int_closure A L) X.
  have [Isub [f /all_and2[fH0 fHk]]] := Ifrac; pose F := subvs_fieldType Ifr;
  pose L0 := fieldOver_fieldExtType Ifr; pose L := aspaceOver Ifr K.
  have Ifrsub : (Ifr <= K)%VS.
    apply/subvP=> x /fHk-[fHx fHxx]; rewrite -(mulKf (fH0 x) x).
    by apply/memvM; rewrite ?memvV; apply/IsubK.
  have LK : L =i K := mem_aspaceOver Ifrsub; have Lnd : ndeg (tr L) L by rewrite -trK_ndeg. 
  have Ifrac1 : is_frac_field (I : pred L0) 1.
    split; first by move => a; rewrite /= trivial_fieldOver; apply/Isub.
    by exists f => k; split => //; rewrite trivial_fieldOver => /fHk.
  have [X Xsize [Xf [Xs Xi]]] := FisK _ L0 _ _ Isubr Iint Ipid Ifrac1 Lnd.
  rewrite -dim_aspaceOver => //; have /eqP <- := Xsize; exists (in_tuple X); split; last first.
    split => m; last by move => /Xi; rewrite /int_closure LK.  
    by rewrite /int_closure -LK; move => /Xs.
  move: Xf; rewrite -{1}(in_tupleE X); move => /freeP-XfL0; apply/freeP => k.
  have [k' kk'] : exists k' : 'I_(size X) -> F, forall i, (k i)%:A = vsval (k' i).
    by exists (fun i => vsproj Ifr (k i)%:A) => i; rewrite vsprojK ?rpredZ ?mem1v.
  pose Ainj := fmorph_inj [rmorphism of in_alg E].
  move => kS i; apply/Ainj => {Ainj} /=; rewrite scale0r kk'; apply/eqP.
  rewrite raddf_eq0; last by apply/subvs_inj.
  by apply/eqP/XfL0; rewrite -{3}kS => {i}; apply/eq_bigr => i _; rewrite -[RHS]mulr_algl kk'.
move => Asubr Aint Apid Afrac1 Lnd; pose n := \dim L; have Amulr : mulr_closed A := Asubr.
have [A0 _] : zmod_closed A := Asubr; have [Asub1 _] := Afrac1.
have AsubL : {subset A <= L} by move => a /Asub1; apply (subvP (sub1v L) a).
have [b1 [b1B b1H]] : exists (b1 : n.-tuple L0), [/\ basis_of L b1 &
  forall i : 'I_n, integral A b1`_i].
  pose b0 := vbasis L; have [f /all_and3-[fH0 fHa fHi]] := frac_field_alg_int Asubr Afrac1.
  pose d := \prod_(i < n) f b0`_i; pose b1 := map_tuple (amulr d) b0.
  exists b1; split; last first => [i|].
    rewrite (nth_map 0) /d; last by rewrite size_tuple.
    rewrite lfunE /= (bigD1 i) //= mulrA; apply/int_mulr_closed => //; first by rewrite mulrC.
    by apply/int_clos_incl => //; rewrite rpred_prod.
  have dun : d \is a GRing.unit by rewrite unitfE /d; apply/prodf_neq0 => i _.
  have lim : (amulr d @: L = L)%VS.
    have dinA : d \in A by rewrite rpred_prod.
    rewrite limg_amulr; apply/eqP; rewrite -dimv_leqif_eq; first by rewrite dim_cosetv_unit.
    by apply/prodv_sub => //; apply/AsubL.
  rewrite -lim limg_basis_of //; last by apply/vbasisP. 
  by have /eqP -> := lker0_amulr dun; rewrite capv0.
have [b2 [/andP[/eqP-b2s b2f] b2H]] : exists (b2 : n.-tuple L0), [/\ basis_of L b2 &
  forall b, b \in L -> integral A b -> forall i, (coord b2 i b)%:A \in A].
  pose b2 := dual_basis L b1; have b2B := dualb_basis Lnd b1B; exists b2; rewrite b2B.
  split => // b biL bint i; suffices <-: tr L b1`_i b = coord b2 i b by rewrite tr_int.
  have -> : tr L b1`_i b = \sum_(j < n) coord b2 j b * tr L b1`_i b2`_j.
    by rewrite {1}(coord_basis b2B biL) linear_sum; apply/eq_bigr => j _; rewrite linearZ.
  rewrite (bigD1 i); have [oi oj //] := dualb_orth Lnd b1B i; rewrite /= oi mulr1 -[RHS]addr0.
  by congr (_ + _); apply/big1 => j jneqi; rewrite (oj j jneqi) mulr0.
have Mbasis k (X : k.-tuple L0) M : free X -> module A M -> submod M (span_mod A X) ->
  exists B, basis_of_mod A M B.
  move: k X M; elim => [X M _ _ Ms | k IH X M Xf [M0 Mm] Ms].
    by exists [::]; rewrite /basis_of_mod nil_free; move: Ms; rewrite tuple0. 
  pose X1 := [tuple of behead X]; pose v := thead X.
  pose M1 := fun m => M m /\ coord X ord0 m = 0.
  pose M2 := fun (a : L0) => exists2 m, M m & (coord X ord0 m)%:A = a.
  have scr r m : r \in A -> exists c, r * m = c *: m.
    by move => /Asub1/vlineP[c ->]; exists c; rewrite mulr_algl.
  have span_coord m : M m -> exists r : (k.+1).-tuple L0,
    [/\ all A r, m = \sum_(i < k.+1) r`_i * X`_i & forall i, (coord X i m)%:A = r`_i].
    have seqF (s : seq L0) : all A s -> exists s', s = [seq c%:A | c <- s'].
      elim: s => [_| a l IHl /= /andP[/Asub1/vlineP[c ->]]]; first by exists [::].
      by move => /IHl[s' ->]; exists (c :: s').
    move => mM; have := Ms m mM; rewrite /span_mod !size_tuple; move => [r rA rS].
    exists r; split => //; have [rF rFr] := seqF r rA => {seqF}; rewrite rFr in rA.
    have rFs : size rF = k.+1 by rewrite -(size_tuple r) rFr size_map.
    have -> : m = \sum_(i < k.+1) rF`_i *: X`_i.
      by rewrite rS; apply/eq_bigr => i _; rewrite rFr (nth_map 0) ?rFs // mulr_algl.
    by move => i; rewrite coord_sum_free // rFr (nth_map 0) ?rFs. 
  have [B1 [B1f [B1s B1A]]] : exists B1, basis_of_mod A M1 B1.
    have X1f : free X1 by move: Xf; rewrite (tuple_eta X) free_cons => /andP[_].
    apply/(IH X1) => //.
      rewrite /module /M1 linear0; split => // a x y aA [xM xfc0] [yM yfc0].
      have := Mm a x y aA xM yM; move: aA => /Asub1/vlineP[r] ->; rewrite mulr_algl => msc.
      by rewrite /M1 linearB linearZ /= xfc0 yfc0 subr0 mulr0.
    move => m [mM mfc0]; have := span_coord m mM; move => [r [rA rS rC]].
    move: mfc0 (rC 0) ->; rewrite scale0r; move => r0; rewrite /span_mod size_tuple.
    exists [tuple of behead r]; first by apply/allP => a /mem_behead/(allP rA).
    by rewrite rS big_ord_recl -r0 mul0r add0r; apply/eq_bigr => i _; rewrite !nth_behead.
  have [a [w wM wC] aG] : exists2 a, M2 a & forall v, M2 v -> exists2 d, d \in A & d * a = v.
    apply/Apid; split.
      move => c [m mM <-]; have := span_coord m mM; move => [r [/all_nthP-rA _ rC]].
      by move: rC ->; apply/rA; rewrite size_tuple.
    split; first by exists 0 => //; rewrite linear0 scale0r.
    move => c x y cA [mx mxM mxC] [my myM myC]; have := Mm c mx my cA mxM myM. 
    move: cA => /Asub1/vlineP[r] ->; rewrite !mulr_algl => mC.
    by exists (r *: mx - my) => //; rewrite linearB linearZ /= scalerBl -scalerA mxC myC.
  pose Ainj := fmorph_inj [rmorphism of in_alg L0].
  have mcM1 m : M m -> exists2 d, d \in A & d * a = (coord X 0 m)%:A.
    by move => mM; apply/aG; exists m.
  case: (eqVneq a 0) => [| an0].
    exists B1; split => //; split => [m mM |]; last by move => m /B1A[mM].
    apply/B1s; split => //; apply/Ainj => /=; have [d _ <-] := mcM1 m mM.
    by rewrite a0 mulr0 scale0r.      
  exists (w :: B1); split.
    rewrite free_cons B1f andbT; move: an0; apply/contra; move: wC <-.
    rewrite -(in_tupleE B1); move => /coord_span ->; apply/eqP.
    rewrite linear_sum big1 ?scale0r => //= i _; rewrite linearZ /=.
    by have [_] := B1A B1`_i (mem_nth 0 (ltn_ord _)) => ->; rewrite mulr0.
  split => [m mM | m]; last by rewrite in_cons; move => /orP; case => [/eqP ->|/B1A[mM]].
  have [d dA dam] := mcM1 m mM; have mdwM1 : M1 (m - d * w).
    split; [have Mdwm := Mm d w m dA wM mM; have := Mm _ _ _ A0 Mdwm Mdwm |].
      by rewrite mul0r sub0r opprB.
    move: dA dam => /Asub1/vlineP[r] -> {d}; rewrite !mulr_algl linearB linearZ /= => rac.
    by apply/Ainj => /=; rewrite scalerBl -scalerA wC rac subrr scale0r.
  have [r rA rS] := B1s _ mdwM1; exists [tuple of d :: r]; first by rewrite /= rA andbT.
  by move: rS => /eqP; rewrite subr_eq addrC => /eqP ->; rewrite /= big_ord_recl.
have [X Xb] : exists X, basis_of_mod A (int_closure A L) X.
  apply/(Mbasis _ b2 _ b2f) => [| m [mL mI]]; first by apply/int_mod_closed.
  pose r : n.-tuple L0 := [tuple (coord b2 i m)%:A | i < n]; rewrite /span_mod size_tuple.
  exists r; have rci (i : 'I_n) : r`_i = (coord b2 i m)%:A by rewrite -tnth_nth tnth_mktuple.
    apply/(all_nthP 0) => i; rewrite size_tuple; move => iB.
    by have -> := rci (Ordinal iB); apply/b2H. 
  move: mL; rewrite -b2s; move => /coord_span ->; apply/eq_bigr => i _.
  by rewrite rci mulr_algl.
exists X => //; move: Xb => [/eqP-Xf [Xs Xg]]; rewrite -Xf eqn_leq; apply/andP; split.
  by apply/dimvS/span_subvP => m /Xg[mL _].
have /andP[/eqP-b1s _] := b1B; rewrite -b1s; apply/dimvS/span_subvP => b /tnthP-[i ->] {b}.
rewrite (tnth_nth 0); have [r /all_tnthP-rA ->] : span_mod A X b1`_i.
  by apply/Xs; rewrite /int_closure (basis_mem b1B) ?mem_nth ?size_tuple => //.
apply/rpred_sum => j _; have := rA j; rewrite (tnth_nth 0); move => /Asub1/vlineP[c ->].
by rewrite mulr_algl; apply/rpredZ/memv_span/mem_nth. 
Qed.

End BasisLemma.