GrowthInGroups: Progress on complex Chevalley's induction

Author: YaelDillies

LeanCamCombi.lean

@@ -31,6 +31,7 @@ import LeanCamCombi.LittlewoodOfford
 import LeanCamCombi.Mathlib.Algebra.Algebra.Operations
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
+import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.BigOperators
 import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
 import LeanCamCombi.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas

LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean

@@ -1,56 +1,70 @@
 import Mathlib.Algebra.Order.Star.Basic
-import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import Mathlib.Data.DFinsupp.WellFounded
-import Mathlib.LinearAlgebra.Charpoly.Basic
-import Mathlib.Order.CompletePartialOrder
-import Mathlib.RingTheory.AdjoinRoot
 import LeanCamCombi.Mathlib.Algebra.Polynomial.Eval
 import LeanCamCombi.Mathlib.Data.Fintype.Card
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Order.RelClasses
 import LeanCamCombi.GrowthInGroups.PolynomialLocalization
 import LeanCamCombi.GrowthInGroups.PrimeSpectrumPolynomial
 
-variable {R M A} [CommRing R] [AddCommGroup M] [Module R M] [CommRing A] [Algebra R A]
+variable {R S M A : Type*} [CommRing R] [CommRing S] [AddCommGroup M] [Module R M] [CommRing A]
+  [Algebra R A]
 
 open Polynomial TensorProduct PrimeSpectrum
+open scoped Pointwise
 
 @[ext]
 structure InductionObj (R) [CommRing R] (n : ℕ) where
   val : Fin n → R[X]
 
-variable {n : ℕ} (S T : InductionObj R n)
+variable {n : ℕ}
 
 instance : CoeFun (InductionObj R n) (fun _ ↦ Fin n → R[X]) := ⟨InductionObj.val⟩
 
 namespace InductionObj
 
-def coeffSubmodule : Submodule ℤ R := Submodule.span ℤ ({1} ∪ ⋃ i, Set.range (S.val i).coeff)
+def coeffSubmodule (e : InductionObj R n) : Submodule ℤ R :=
+  .span ℤ ({1} ∪ ⋃ i, Set.range (e.val i).coeff)
 
-lemma one_le_coeffSubmodule : 1 ≤ S.coeffSubmodule := by
+lemma coeffSubmodule_mapRingHom_comp (e : InductionObj R n) (f : R →+* S) :
+    ({ val := mapRingHom f ∘ e.val } : InductionObj S n).coeffSubmodule
+      = e.coeffSubmodule.map f.toIntAlgHom.toLinearMap := by
+  simp [coeffSubmodule, Submodule.map_span, Set.image_insert_eq, Set.image_iUnion, ← Set.range_comp,
+    coeff_map_eq_comp]
+
+variable {e T : InductionObj R n}
+
+lemma one_le_coeffSubmodule : 1 ≤ e.coeffSubmodule := by
   rw [Submodule.one_eq_span, Submodule.span_le, Set.singleton_subset_iff]
   exact Submodule.subset_span (.inl rfl)
 
 variable (n) in
 abbrev DegreeType := (Fin n → WithBot ℕ) ×ₗ Prop
 
+variable (S) in
 def degree : DegreeType n :=
-  toLex (Polynomial.degree ∘ S.val, ¬ ∃ i, (S.val i).Monic ∧
-    ∀ j, S.val j ≠ 0 → (S.val i).degree ≤ (S.val j).degree)
+  toLex (Polynomial.degree ∘ e.val, ¬ ∃ i, (e.val i).Monic ∧
+    ∀ j, e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree)
 
-@[simp] lemma ofLex_degree_fst (i) : (ofLex S.degree).fst i = (S.val i).degree := rfl
-lemma ofLex_degree_snd : (ofLex S.degree).snd = ¬ ∃ i, (S.val i).Monic ∧
-    ∀ j, S.val j ≠ 0 → (S.val i).degree ≤ (S.val j).degree := rfl
+@[simp] lemma ofLex_degree_fst (i) : (ofLex e.degree).fst i = (e.val i).degree := rfl
+lemma ofLex_degree_snd : (ofLex e.degree).snd = ¬ ∃ i, (e.val i).Monic ∧
+    ∀ j, e.val j ≠ 0 → (e.val i).degree ≤ (e.val j).degree := rfl
 
-def degBound : ℕ := 2 ^ ∑ i, (S.val i).natDegree
+def degBound : ℕ := 2 ^ ∑ i, (e.val i).natDegree
 
-def exponentBound : ℕ := S.degBound ^ S.degBound
+def exponentBound : ℕ := e.degBound ^ e.degBound
 
-def InductionStatement (R) (n) [CommRing R] (S : InductionObj R n) : Prop :=
+def InductionStatement (R) (n) [CommRing R] (e : InductionObj R n) : Prop :=
   ∀ f, ∃ T : Finset (Σ n, R × (Fin n → R)),
-    comap C '' (zeroLocus (Set.range S.val) \ zeroLocus {f}) =
+    comap C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) =
       ⋃ C ∈ T, (zeroLocus (Set.range C.2.2) \ zeroLocus {C.2.1}) ∧
-    ∀ C ∈ T, C.1 ≤ S.degBound ∧ ∀ i, C.2.2 i ∈ S.coeffSubmodule ^ S.exponentBound
+    ∀ C ∈ T, C.1 ≤ e.degBound ∧ ∀ i, C.2.2 i ∈ e.coeffSubmodule ^ e.exponentBound
+
+open Submodule in
+lemma coeffSubmodule_smul (e : InductionObj R n) (f : R →+* S) (a : R) [Invertible (f a)] :
+    ({ val := ⅟(f a) • mapRingHom f ∘ e.val } : InductionObj S n).coeffSubmodule =
+      ⅟(f a) ^ e.degBound • (span ℤ ({a} ∪ ⋃ i, Set.range (e.val i).coeff)).map f.toIntAlgHom.toLinearMap := by
+  sorry -- probably useless
 
 universe u
 
@@ -150,7 +164,7 @@ lemma foo_induction (n : ℕ)
 universe v
 
 lemma comap_C_eq_comap_quotient_union_comap_localization (s : Set (PrimeSpectrum R[X])) (c : R) :
-    comap C '' s =
+    .comap C '' s =
       comap (Ideal.Quotient.mk (.span {c})) '' (comap C ''
         (comap (mapRingHom (Ideal.Quotient.mk _)) ⁻¹' s)) ∪
       comap (algebraMap R (Localization.Away c)) '' (comap C ''
@@ -198,6 +212,7 @@ lemma Ideal.span_range_update_divByMonic {ι : Type*} [DecidableEq ι]
       · exact ⟨i, Function.update_noteq hij _ _⟩
     exact Ideal.subset_span ⟨k, Function.update_noteq (.symm hjk) _ _⟩
 
+open Polynomial IsLocalization Localization in
 lemma induction_aux (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n)
       (hi : c = (e.1 i).leadingCoeff) :
       InductionStatement (Localization.Away c) n
@@ -206,9 +221,13 @@ lemma induction_aux (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n)
       InductionStatement (R ⧸ Ideal.span {c}) n ⟨mapRingHom (algebraMap _ _) ∘ e.val⟩ →
         InductionStatement R n e := by
   intro H₁ H₂ f
-  obtain ⟨T₁, hT₁, HT₁⟩ := H₁ (mapRingHom (algebraMap _ _) f)
-  obtain ⟨T₂, hT₂, HT₂⟩ := H₂ (mapRingHom (algebraMap _ _) f)
-  simp only [coe_mapRingHom] at HT₁
+  obtain ⟨T₁, hT₁⟩ := H₁ (mapRingHom (algebraMap _ _) f)
+  obtain ⟨T₂, hT₂⟩ := H₂ (mapRingHom (algebraMap _ _) f)
+  simp only [forall_and] at hT₁ hT₂
+  obtain ⟨hT₁, hT₁deg, hT₁span⟩ := hT₁
+  obtain ⟨hT₂, hT₂deg, hT₂span⟩ := hT₂
+  rw [coeffSubmodule_mapRingHom_comp, ← Submodule.map_pow] at hT₂span
+  choose l₂ hl₂ using hT₂span
   sorry
 
 lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus {R} [CommRing R] {n}

LeanCamCombi/Mathlib/Algebra/Algebra/Operations.lean

@@ -1,9 +1,9 @@
 import Mathlib.Algebra.Algebra.Operations
 
-namespace Submodule
-
 open scoped Pointwise
 
+namespace Submodule
+
 variable {R : Type*} {M : Type*}
 
 variable [CommSemiring R] [Semiring M] [Algebra R M]
@@ -24,3 +24,27 @@ lemma pow_mono (hst : s ≤ t) (ht : 1 ≤ t) {m n : ℕ} (hmn : m ≤ n) : s ^
   (pow_le_pow_left' hst _).trans (pow_le_pow_right' ht hmn)
 
 end Submodule
+
+namespace Submodule
+variable {R S : Type*} [CommRing R] [CommRing S]
+
+lemma exists_lift_localization {s : Set R} {D : ℕ} {c : R} {f : R →+* S} [Invertible (f c)]
+    (x : S) (hx : x ∈ span ℤ ({1} ∪ ⅟(f c) • f '' s) ^ D) :
+    ∃ y ∈ span ℤ ({c} ∪ s) ^ D, f y = x * f c ^ D := by
+  induction hx using Submodule.pow_induction_on_left' with
+  | algebraMap => simp
+  | add x₁ x₂ D hx₁ hx₂ ih₁ ih₂ =>
+    obtain ⟨y₁, hy₁, hyx₁⟩ := ih₁
+    obtain ⟨y₂, hy₂, hyx₂⟩ := ih₂
+    refine ⟨y₁ + y₂, add_mem hy₁ hy₂, ?_⟩
+    simp [add_mul, hyx₁, hyx₂]
+  | mem_mul m hm D x hx ih =>
+    obtain ⟨n, hn, hnm⟩ : f c * m ∈ (span ℤ ({c} ∪ s)).map f.toIntAlgHom.toLinearMap := by
+      simpa [map_span, span_mul_span, Set.image_insert_eq, ← Set.image_smul, Set.image_image]
+        using mul_mem_mul (mem_span_singleton_self (f c)) hm
+    obtain ⟨y, hy, hyx⟩ := ih
+    dsimp at hnm
+    rw [pow_succ']
+    exact ⟨n * y, mul_mem_mul hn hy, by simp [hnm, hyx]; ring⟩
+
+end Submodule

LeanCamCombi/Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

@@ -0,0 +1,20 @@
+import Mathlib.Data.Set.Pointwise.BigOperators
+import Mathlib.Data.Set.Pointwise.ListOfFn
+
+open scoped Pointwise
+
+namespace Set
+variable {α : Type*}
+
+section CommMonoid
+variable [CommMonoid α] {s t : Set α} {a : α} {n : ℕ}
+
+@[to_additive]
+lemma mem_pow_iff_prod : ∀ {n}, a ∈ s ^ n ↔ ∃ f : Fin n → α, (∀ i, f i ∈ s) ∧ ∏ i, f i = a
+  | 0 => by simp [eq_comm]
+  | n + 1 => by
+    simp_rw [pow_succ, mem_mul]
+    sorry
+
+end CommMonoid
+end Set

LeanCamCombi/Mathlib/Algebra/Polynomial/Eval.lean

@@ -2,5 +2,11 @@ import Mathlib.Algebra.Polynomial.Eval
 
 namespace Polynomial
 
-lemma mapRingHom_comp_C {R S} [CommRing R] [CommRing S] (f : R →+* S) : 
+lemma mapRingHom_comp_C {R S} [CommRing R] [CommRing S] (f : R →+* S) :
     (mapRingHom f).comp C = C.comp f := by ext; simp
+
+variable {R S : Type*} [Semiring R] [Semiring S]
+
+-- TODO: Rename `coeff_map` to `coeff_map_apply`?
+lemma coeff_map_eq_comp (p : R[X]) (f : R →+* S) : (p.map f).coeff = f ∘ p.coeff := by
+  ext n; exact coeff_map ..