Commit b5eb6ae

import Mathlib

import Diaz.Platform

namespace Diaz

open Complex ComplexConjugate

namespace RC1_FL

theorem roy_field_lifts_logAlg_add {u v : ℂ} (hu : u ∈ LogAlg) (hv : v ∈ LogAlg) : u + v ∈ LogAlg := by

show IsAlgebraic ℚ (Complex.exp (u + v))

rw [Complex.exp_add]

exact mem_Qbar_iff.mp (Qbar.mul_mem (mem_Qbar_iff.mpr hu) (mem_Qbar_iff.mpr hv))

theorem roy_field_lifts_logAlg_zero : (0 : ℂ) ∈ LogAlg := by

show IsAlgebraic ℚ (Complex.exp 0)

rw [Complex.exp_zero]

exact isAlgebraic_one

theorem logAlg_ratMul {g : ℂ} (hg : g ∈ LogAlg) (r : ℚ) : (r : ℂ) * g ∈ LogAlg := by

show IsAlgebraic ℚ (Complex.exp ((r : ℂ) * g))

have h1 : Complex.exp ((r : ℂ) * g) ^ r.den = Complex.exp g ^ r.num := by

rw [← Complex.exp_nat_mul, ← Complex.exp_int_mul]

congr 1

have hd : (r.den : ℂ) ≠ 0 := by exact_mod_cast r.den_ne_zero

rw [Rat.cast_def]

field_simp

have h2 : Complex.exp g ^ r.num ∈ Qbar := zpow_mem (mem_Qbar_iff.mpr hg) _

exact IsAlgebraic.of_pow r.den_pos (h1 ▸ mem_Qbar_iff.mp h2)

theorem rep (K : IntermediateField ℚ ℂ) [FiniteDimensional ℚ K] {c : ℂ} (hc : c ∈ K) :

c = ∑ k, (((Module.finBasis ℚ K).repr ⟨c, hc⟩ k : ℚ) : ℂ) *

((Module.finBasis ℚ K k : K) : ℂ) := by

have h := congrArg (fun w : K => (w : ℂ)) ((Module.finBasis ℚ K).sum_repr ⟨c, hc⟩)

simp only [IntermediateField.coe_sum] at h

refine h.symm.trans (Finset.sum_congr rfl (fun k _ => ?_))

rw [IntermediateField.coe_smul, Rat.smul_def]

theorem mem_span_of_mem (K : IntermediateField ℚ ℂ) [FiniteDimensional ℚ K] {c : ℂ}

(hc : c ∈ K) :

c ∈ Submodule.span ℚ (Set.range fun k => ((Module.finBasis ℚ K k : K) : ℂ)) := by

rw [rep K hc]

refine Submodule.sum_mem _ fun k _ => ?_

rw [← Rat.smul_def]

exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨k, rfl⟩)

def roy_field_lifts_Shape (K : IntermediateField ℚ ℂ) {m : ℕ} (ω : Fin m → ℂ) (w : ℂ) : Prop :=

∃ u ∈ K, ∃ v : Fin m → ℂ, (∀ k, v k ∈ LogAlg) ∧ w = u + ∑ k, ω k * v k

theorem roy_field_lifts_shape_zero (K : IntermediateField ℚ ℂ) {m : ℕ} (ω : Fin m → ℂ) : roy_field_lifts_Shape K ω 0 :=

⟨0, K.zero_mem, 0, fun _ => roy_field_lifts_logAlg_zero, by simp⟩

theorem roy_field_lifts_shape_add (K : IntermediateField ℚ ℂ) {m : ℕ} (ω : Fin m → ℂ) {w w' : ℂ}

(hw : roy_field_lifts_Shape K ω w) (hw' : roy_field_lifts_Shape K ω w') : roy_field_lifts_Shape K ω (w + w') := by

obtain ⟨u, hu, v, hv, rfl⟩ := hw

obtain ⟨u', hu', v', hv', rfl⟩ := hw'

refine ⟨u + u', K.add_mem hu hu', v + v', fun k => roy_field_lifts_logAlg_add (hv k) (hv' k), ?_⟩

simp only [Pi.add_apply, mul_add, Finset.sum_add_distrib]

ring

theorem roy_field_lifts_shape_term (K : IntermediateField ℚ ℂ) [FiniteDimensional ℚ K] {c g : ℂ} (hc : c ∈ K)

(hg : g ∈ insert (1 : ℂ) LogAlg) :

roy_field_lifts_Shape K (fun k => ((Module.finBasis ℚ K k : K) : ℂ)) (c * g) := by

rcases hg with rfl | hg

· exact ⟨c, hc, 0, fun _ => roy_field_lifts_logAlg_zero, by simp⟩

· refine ⟨0, K.zero_mem, fun k => (((Module.finBasis ℚ K).repr ⟨c, hc⟩ k : ℚ) : ℂ) * g,

fun k => logAlg_ratMul hg _, ?_⟩

refine (congrArg (· * g) (rep K hc)).trans ?_

rw [zero_add, Finset.sum_mul]

exact Finset.sum_congr rfl (fun k _ => by ring)

end RC1_FL

open RC1_FL in

theorem roy_field_lifts {d ℓ : ℕ} (z : Fin ℓ → Fin d → ℂ) (hz : ∀ i j, z i j ∈ LogAlgTilde) :

∃ (m : ℕ) (ω : Fin m → ℂ) (η : Fin m × Fin ℓ → (Fin d → ℂ) × (Fin m × Fin d → ℂ)),

0 < m ∧ LinearIndependent ℚ ω ∧ (∀ a, ω a ∈ Qbar) ∧

(1 : ℂ) ∈ Submodule.span ℚ (Set.range ω) ∧

(∀ a b, ω a * ω b ∈ Submodule.span ℚ (Set.range ω)) ∧

(∀ p, (∀ i, (η p).1 i ∈ Submodule.span ℚ (Set.range ω)) ∧ ∀ q, (η p).2 q ∈ LogAlg) ∧

∀ p, (LinearMap.pi fun i : Fin d =>

(LinearMap.proj i : (Fin d → ℂ) →ₗ[ℂ] ℂ) ∘ₗ LinearMap.fst ℂ (Fin d → ℂ) (Fin m × Fin d → ℂ)

+ ∑ k, ω k • (LinearMap.proj (k, i) : (Fin m × Fin d → ℂ) →ₗ[ℂ] ℂ) ∘ₗ

LinearMap.snd ℂ (Fin d → ℂ) (Fin m × Fin d → ℂ)) (η p) = ω p.1 • z p.2 := by

choose n f g hfg using fun ij : Fin ℓ × Fin d => Submodule.mem_span_set'.mp (hz ij.1 ij.2)

set S : Set ℂ :=

Set.range (fun p : (Σ ij : Fin ℓ × Fin d, Fin (n ij)) => ((f p.1 p.2 : Qbar) : ℂ))

have hSQ : ∀ c ∈ S, c ∈ Qbar := by

rintro _ ⟨p, rfl⟩

exact (f p.1 p.2).2

set K := IntermediateField.adjoin ℚ S

have : FiniteDimensional ℚ K :=

IntermediateField.finiteDimensional_adjoin (fun c hc => (mem_Qbar_iff.mp (hSQ c hc)).isIntegral)

have hK : ∀ c ∈ K, c ∈ Qbar := fun c hc =>

mem_Qbar_iff.mpr (IntermediateField.isAlgebraic_iff.mp

(Algebra.IsAlgebraic.isAlgebraic (⟨c, hc⟩ : K)))

set ω : Fin (Module.finrank ℚ K) → ℂ := fun k => ((Module.finBasis ℚ K k : K) : ℂ) with hω

have hkey : ∀ (a : Fin (Module.finrank ℚ K)) (i : Fin ℓ) (j : Fin d),

roy_field_lifts_Shape K ω (ω a * z i j) := by

intro a i j

rw [← hfg (i, j), Finset.mul_sum]

refine Finset.sum_induction _ (roy_field_lifts_Shape K ω) (fun _ _ => roy_field_lifts_shape_add K ω) (roy_field_lifts_shape_zero K ω) ?_

intro l _

rw [Subfield.smul_def, smul_eq_mul, ← mul_assoc]

have hfK : ((f (i, j) l : Qbar) : ℂ) ∈ K :=

IntermediateField.subset_adjoin _ _ ⟨⟨(i, j), l⟩, rfl⟩

exact roy_field_lifts_shape_term K (K.mul_mem (Module.finBasis ℚ K a).2 hfK) (g (i, j) l).2

choose U hU V hV hUV using hkey

refine ⟨Module.finrank ℚ K, ω, fun p => (fun j => U p.1 p.2 j, fun kj => V p.1 p.2 kj.2 kj.1),

Module.finrank_pos, ?_, fun a => hK _ (Module.finBasis ℚ K a).2,

mem_span_of_mem K K.one_mem,

fun a b => mem_span_of_mem K (K.mul_mem (Module.finBasis ℚ K a).2 (Module.finBasis ℚ K b).2),

fun p => ⟨fun j => mem_span_of_mem K (hU _ _ _), fun kj => hV _ _ _ _⟩, ?_⟩

· exact (Module.finBasis ℚ K).linearIndependent.map' K.val.toLinearMap

(LinearMap.ker_eq_bot.mpr Subtype.val_injective)

· rintro ⟨a, i⟩

funext j

simp only [LinearMap.pi_apply, LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply,

LinearMap.coe_fst, LinearMap.coe_snd, LinearMap.coe_proj, Function.eval,

LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, Pi.smul_apply]

exact (hUV a i j).symm

end Diaz

import Mathlib

import Diaz.Platform

namespace Diaz

open Complex ComplexConjugate

namespace RC1_IK

noncomputable def Ups1 (d m : ℕ) (ω : Fin m → ℂ) : (Fin m × Fin d → ℂ) →ₗ[ℂ] (Fin d → ℂ) :=

LinearMap.pi fun i : Fin d => ∑ k, ω k • (LinearMap.proj (k, i) : (Fin m × Fin d → ℂ) →ₗ[ℂ] ℂ)

theorem Ups1_apply {d m : ℕ} (ω : Fin m → ℂ) (y : Fin m × Fin d → ℂ) (i : Fin d) :

Ups1 d m ω y i = ∑ k, ω k * y (k, i) := by

simp [Ups1, LinearMap.sum_apply]

def Lq {ι : Type} [Fintype ι] {q : ℕ} (φ : Fin q → ι → ℤ) : Submodule ℚ (ι → ℚ) where

carrier := {r | ∀ k, ∑ i, (φ k i : ℚ) * r i = 0}

add_mem' {r s} hr hs k := by

simp only [Set.mem_ofPred_eq, Pi.add_apply, mul_add, Finset.sum_add_distrib] at *

rw [hr k, hs k, add_zero]

zero_mem' k := by simp

smul_mem' c r hr k := by

simp only [Set.mem_ofPred_eq, Pi.smul_apply, smul_eq_mul] at *

rw [← mul_zero c, ← hr k, Finset.mul_sum]

exact Finset.sum_congr rfl fun _ _ => by ring

def castL {ι : Type} : (ι → ℚ) →ₗ[ℚ] (ι → ℂ) where

toFun r i := (r i : ℂ)

map_add' r s := by funext i; simp

map_smul' c r := by funext i; simp [Rat.smul_def]

theorem castL_mem {ι : Type} [Fintype ι] {q : ℕ} (φ : Fin q → ι → ℤ) {r : ι → ℚ}

(hr : r ∈ Lq φ) (k : Fin q) : ∑ i, (φ k i : ℂ) * castL r i = 0 := by

have := congrArg (fun x : ℚ => (x : ℂ)) (hr k)

simpa [castL] using this

theorem mem_span_of_ker {ι : Type} [Fintype ι] {q : ℕ} (φ : Fin q → ι → ℤ) (y : ι → ℂ)

(hy : ∀ k, ∑ i, (φ k i : ℂ) * y i = 0) :

y ∈ Submodule.span ℂ (castL '' (Lq φ : Set (ι → ℚ))) := by

set C := Submodule.span ℚ (Set.range y)

have : FiniteDimensional ℚ C := FiniteDimensional.span_of_finite ℚ (Set.finite_range y)

set c := Module.finBasis ℚ C

set e := c.equivFun

let yC : ι → C := fun i => ⟨y i, Submodule.subset_span ⟨i, rfl⟩⟩

have hsum0 : ∀ k, ∑ i, (φ k i : ℚ) • yC i = 0 := by

intro k

apply Subtype.ext

simp only [Submodule.coe_sum, Submodule.coe_smul, Submodule.coe_zero, yC, Rat.smul_def,

Rat.cast_intCast]

exact hy k

have hr : ∀ t, (fun i => e (yC i) t) ∈ Lq φ := by

intro t k

have := congrArg (fun x => e x t) (hsum0 k)

simpa [map_sum, map_smul] using this

have hyexp : y = ∑ t, ((c t : C) : ℂ) • castL (fun i => e (yC i) t) := by

funext i

have := congrArg Subtype.val (c.sum_equivFun (yC i))

simp only [Submodule.coe_sum, Submodule.coe_smul, Rat.smul_def, yC] at this

rw [Finset.sum_apply]

refine this.symm.trans (Finset.sum_congr rfl fun t _ => ?_)

simp [castL, e, yC, mul_comm]

rw [hyexp]

exact Submodule.sum_mem _ fun t _ =>

Submodule.smul_mem _ _ (Submodule.subset_span ⟨_, hr t, rfl⟩)

theorem finrank_span_cast_le {ι : Type} [Fintype ι] (L : Submodule ℚ (ι → ℚ)) :

Module.finrank ℂ ↥(Submodule.span ℂ (castL '' (L : Set (ι → ℚ)))) ≤ Module.finrank ℚ L := by

set b := Module.finBasis ℚ L

have hle : Submodule.span ℂ (castL '' (L : Set (ι → ℚ))) ≤

Submodule.span ℂ (Set.range fun j => castL ((b j : L) : ι → ℚ)) := by

rw [Submodule.span_le]

rintro _ ⟨r, hr, rfl⟩

have h := congrArg (fun x : L => castL (x : ι → ℚ)) (b.sum_equivFun ⟨r, hr⟩)

simp only [Submodule.coe_sum, Submodule.coe_smul, map_sum, map_smul] at h

rw [← h]

exact Submodule.sum_mem _ fun j _ =>

Submodule.smul_of_tower_mem _ _ (Submodule.subset_span ⟨j, rfl⟩)

refine (Submodule.finrank_mono hle).trans ?_

have := finrank_range_le_card (R := ℂ) (fun j => castL ((b j : L) : ι → ℚ))

simpa [Set.finrank] using this

theorem exists_coords {d : ℕ} (W : Submodule ℂ (Fin d → ℂ)) :

∃ (κ : Type) (a : κ → Fin d) (_ : Fintype κ), Fintype.card κ ≤ Module.finrank ℂ W ∧

∀ x ∈ W, (∀ j, x (a j) = 0) → x = 0 := by

let f : Fin d → Module.Dual ℂ W := fun i => (LinearMap.proj i).comp W.subtype

obtain ⟨κ, a, ha, hspan, hli⟩ := exists_linearIndependent' ℂ f

have : Fintype κ := Fintype.ofInjective a ha

refine ⟨κ, a, inferInstance, ?_, ?_⟩

· have := hli.fintype_card_le_finrank

rwa [Subspace.dual_finrank_eq] at this

· intro x hx h0

have hall : ∀ g ∈ Submodule.span ℂ (Set.range (f ∘ a)), g ⟨x, hx⟩ = 0 := by

intro g hg

induction hg using Submodule.span_induction with

| mem g hg => obtain ⟨j, rfl⟩ := hg; exact h0 j

| zero => rfl

| add g h _ _ hg hh => simp [hg, hh]

| smul c g _ hg => simp [hg]

funext i

have := hall (f i) (hspan ▸ Submodule.subset_span ⟨i, rfl⟩)

simpa [f] using this

theorem finrank_le_of_maps {d m : ℕ} (ω : Fin m → ℂ) (hω : LinearIndependent ℚ ω)

(L : Submodule ℚ (Fin m × Fin d → ℚ)) (W : Submodule ℂ (Fin d → ℂ))

(hW : ∀ r ∈ L, Ups1 d m ω (castL r) ∈ W) :

Module.finrank ℚ L ≤ m * Module.finrank ℂ W := by

obtain ⟨κ, a, _, hcard, hinj⟩ := exists_coords W

let G : (Fin m × Fin d → ℚ) →ₗ[ℚ] (κ × Fin m → ℚ) :=

{ toFun := fun r p => r (p.2, a p.1)

map_add' := fun _ _ => rfl

map_smul' := fun _ _ => rfl }

have hG : Function.Injective (G ∘ₗ L.subtype) := by

rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']

intro r hr

have hr' : ∀ j k, (r : Fin m × Fin d → ℚ) (k, a j) = 0 := fun j k =>

congrFun hr (j, k)

have h1 : Ups1 d m ω (castL (r : Fin m × Fin d → ℚ)) = 0 := by

refine hinj _ (hW r r.2) fun j => ?_

rw [Ups1_apply]

simp [castL, hr' j]

apply Subtype.ext

funext ⟨k, i⟩

have h2 := congrFun h1 i

rw [Ups1_apply] at h2

have h3 := Fintype.linearIndependent_iff.mp hω (fun k => (r : Fin m × Fin d → ℚ) (k, i))

(by simpa [Rat.smul_def, castL, mul_comm] using h2) k

simpa using h3

have := LinearMap.finrank_le_finrank_of_injective hG

rw [Module.finrank_fintype_fun_eq_card, Fintype.card_prod, Fintype.card_fin] at this

calc Module.finrank ℚ L ≤ Fintype.card κ * m := this

_ ≤ Module.finrank ℂ W * m := Nat.mul_le_mul_right _ hcard

_ = m * Module.finrank ℂ W := Nat.mul_comm _ _

end RC1_IK

open RC1_IK in

theorem roy_intKer_image {d m q : ℕ} (ω : Fin m → ℂ) (hωQ : LinearIndependent ℚ ω)

(hωalg : ∀ a, ω a ∈ Qbar) (φ : Fin q → Fin m × Fin d → ℤ) (L₁ : Submodule ℂ (Fin m × Fin d → ℂ))

(hL₁ : ∀ v, v ∈ L₁ ↔ ∀ k, ∑ i, (φ k i : ℂ) * v i = 0) :

Module.finrank ℂ ↥(L₁) ≤ m * Module.finrank ℂ ↥(L₁.map (LinearMap.pi fun i : Fin d =>

∑ k, ω k • (LinearMap.proj (k, i) : (Fin m × Fin d → ℂ) →ₗ[ℂ] ℂ))) ∧

Submodule.span ℂ {v : Fin d → ℂ | v ∈ L₁.map (LinearMap.pi fun i : Fin d =>

∑ k, ω k • (LinearMap.proj (k, i) : (Fin m × Fin d → ℂ) →ₗ[ℂ] ℂ)) ∧ ∀ i, v i ∈ Qbar} = L₁.map (LinearMap.pi fun i : Fin d =>

∑ k, ω k • (LinearMap.proj (k, i) : (Fin m × Fin d → ℂ) →ₗ[ℂ] ℂ)) := by

change Module.finrank ℂ ↥L₁ ≤ m * Module.finrank ℂ ↥(L₁.map (Ups1 d m ω)) ∧

Submodule.span ℂ {v : Fin d → ℂ | v ∈ L₁.map (Ups1 d m ω) ∧ ∀ i, v i ∈ Qbar} =

L₁.map (Ups1 d m ω)

have hcastL : ∀ r ∈ Lq φ, castL r ∈ L₁ := fun r hr => (hL₁ _).mpr (castL_mem φ hr)

have hspan : L₁ = Submodule.span ℂ (castL '' (Lq φ : Set (Fin m × Fin d → ℚ))) := by

apply le_antisymm

· intro y hy

exact mem_span_of_ker φ y ((hL₁ y).mp hy)

· rw [Submodule.span_le]

rintro _ ⟨r, hr, rfl⟩

exact hcastL r hr

refine ⟨?_, ?_⟩

· calc Module.finrank ℂ ↥L₁ ≤ Module.finrank ℚ (Lq φ) := by

rw [hspan]; exact finrank_span_cast_le _

_ ≤ m * Module.finrank ℂ ↥(L₁.map (Ups1 d m ω)) :=

finrank_le_of_maps ω hωQ _ _ fun r hr => Submodule.mem_map_of_mem (hcastL r hr)

· apply le_antisymm

· rw [Submodule.span_le]

exact fun v hv => hv.1

· conv_lhs => rw [hspan]

rw [Submodule.map_span]

apply Submodule.span_mono

rintro _ ⟨_, ⟨r, hr, rfl⟩, rfl⟩

refine ⟨Submodule.mem_map_of_mem (hcastL r hr), fun i => ?_⟩

rw [Ups1_apply]

exact Qbar.sum_mem fun k _ => Qbar.mul_mem (hωalg k) (SubfieldClass.ratCast_mem Qbar _)

end Diaz