diff --git a/LeanCamCombi.lean b/LeanCamCombi.lean index 5c83bcb6f3..720cd49f6e 100644 --- a/LeanCamCombi.lean +++ b/LeanCamCombi.lean @@ -10,13 +10,7 @@ import LeanCamCombi.ExtrProbCombi.Containment import LeanCamCombi.ExtrProbCombi.GiantComponent import LeanCamCombi.GraphTheory.ExampleSheet1 import LeanCamCombi.GraphTheory.ExampleSheet2 -import LeanCamCombi.GroupMarking -import LeanCamCombi.GrowthInGroups.ApproximateSubgroup -import LeanCamCombi.GrowthInGroups.Chevalley import LeanCamCombi.GrowthInGroups.ChevalleyComplex -import LeanCamCombi.GrowthInGroups.Constructible -import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum -import LeanCamCombi.GrowthInGroups.ConstructibleSetData import LeanCamCombi.GrowthInGroups.Lecture1 import LeanCamCombi.GrowthInGroups.Lecture2 import LeanCamCombi.GrowthInGroups.Lecture3 @@ -25,13 +19,12 @@ import LeanCamCombi.Impact import LeanCamCombi.Kneser.Kneser import LeanCamCombi.Kneser.KneserRuzsa import LeanCamCombi.Kneser.MulStab -import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees -import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv import LeanCamCombi.Mathlib.Analysis.Convex.Exposed import LeanCamCombi.Mathlib.Analysis.Convex.Extreme import LeanCamCombi.Mathlib.Analysis.Convex.Independence import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic +import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic @@ -41,7 +34,6 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph import LeanCamCombi.Mathlib.Data.List.DropRight import LeanCamCombi.Mathlib.Data.Multiset.Basic -import LeanCamCombi.Mathlib.Data.Set.Image import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional @@ -51,7 +43,6 @@ import LeanCamCombi.Mathlib.Order.Flag import LeanCamCombi.Mathlib.Order.Partition.Finpartition import LeanCamCombi.Mathlib.Order.RelIso.Group import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions -import LeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.Topology import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated import LeanCamCombi.MetricBetween import LeanCamCombi.MinkowskiCaratheodory diff --git a/LeanCamCombi/GroupMarking.lean b/LeanCamCombi/GroupMarking.lean deleted file mode 100644 index 8f57d21a6d..0000000000 --- a/LeanCamCombi/GroupMarking.lean +++ /dev/null @@ -1,273 +0,0 @@ -/- -Copyright (c) 2023 Yaël Dillies. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yaël Dillies --/ -import Mathlib.Analysis.Normed.Group.Basic -import Mathlib.GroupTheory.FreeGroup.Reduce - -/-! -# Marked groups - -This file defines group markings and induces a norm on marked groups. - -## Main declarations - -* `GroupMarking G S`: Marking of the group `G` by a type `S`, namely a surjective monoid - homomorphism `FreeGroup S →* G`. -* `MarkedGroup`: If `m : GroupMarking G S`, then `MarkedGroup m` is a type synonym for `G` - endowed with the metric coming from `m`. -* `MarkedGroup.instNormedGroup`: A marked group is normed by its marking. - -## TODO - -Protect `List.le_antisymm` --/ - -open Function List Nat - -variable {G S : Type*} [Group G] - -/-- A marking of an additive group is a generating family of elements. -/ -structure AddGroupMarking (G S : Type*) [AddGroup G] extends FreeAddGroup S →+ G where - toFun_surjective : Surjective toFun - -/-- A marking of a group is a generating family of elements. -/ -@[to_additive] -structure GroupMarking (G S : Type*) [Group G] extends FreeGroup S →* G where - toFun_surjective : Surjective toFun - -/-- Reinterpret a marking of `G` by `S` as an additive monoid homomorphism `free_add_group S →+ G`. --/ -add_decl_doc AddGroupMarking.toAddMonoidHom - -/-- Reinterpret a marking of `G` by `S` as a monoid homomorphism `FreeGroup S →+ G`. -/ -add_decl_doc GroupMarking.toMonoidHom - -namespace GroupMarking - -@[to_additive] -instance instFunLike : FunLike (GroupMarking G S) (FreeGroup S) G where - coe f := f.toFun - coe_injective' := by rintro ⟨⟨⟨_, _⟩, _⟩, _⟩; congr! - -@[to_additive] -instance instMonoidHomClass : MonoidHomClass (GroupMarking G S) (FreeGroup S) G where - map_mul f := f.map_mul' - map_one f := f.map_one' - -@[to_additive] -lemma coe_surjective (m : GroupMarking G S) : Surjective m := m.toFun_surjective - -end GroupMarking - -/-- The trivial group marking. -/ -@[to_additive "The trivial additive group marking."] -def GroupMarking.refl : GroupMarking G G := - { FreeGroup.lift id with toFun_surjective := fun x => ⟨FreeGroup.of x, FreeGroup.lift.of⟩ } - -@[to_additive] instance : Inhabited (GroupMarking G G) := ⟨.refl⟩ - -variable {m : GroupMarking G S} - -set_option linter.unusedVariables false in -/-- A type synonym of `G`, tagged with a group marking. -/ -@[to_additive "A type synonym of `G`, tagged with an additive group marking."] -def MarkedGroup (m : GroupMarking G S) : Type _ := G - -@[to_additive] instance MarkedGroup.instGroup : Group (MarkedGroup m) := ‹Group G› - -/-- "Identity" isomorphism between `G` and a group marking of it. -/ -@[to_additive "\"Identity\" isomorphism between `G` and an additive group marking of it."] -def toMarkedGroup : G ≃* MarkedGroup m := .refl _ - -/-- "Identity" isomorphism between a group marking of `G` and itself. -/ -@[to_additive "\"Identity\" isomorphism between an additive group marking of `G` and itself."] -def ofMarkedGroup : MarkedGroup m ≃* G := .refl _ - -@[to_additive (attr := simp)] -lemma toMarkedGroup_symm_eq : (toMarkedGroup : G ≃* MarkedGroup m).symm = ofMarkedGroup := rfl - -@[to_additive (attr := simp)] -lemma ofMarkedGroup_symm_eq : (ofMarkedGroup : MarkedGroup m ≃* G).symm = toMarkedGroup := rfl - -@[to_additive (attr := simp)] -lemma toMarkedGroup_ofMarkedGroup (a) : toMarkedGroup (ofMarkedGroup (a : MarkedGroup m)) = a := rfl - -@[to_additive (attr := simp)] -lemma ofMarkedGroup_toMarkedGroup (a) : ofMarkedGroup (toMarkedGroup a : MarkedGroup m) = a := rfl - -@[to_additive (attr := simp)] -lemma toMarkedGroup_inj {a b} : (toMarkedGroup a : MarkedGroup m) = toMarkedGroup b ↔ a = b := .rfl - -@[to_additive (attr := simp)] -lemma ofMarkedGroup_inj {a b : MarkedGroup m} : ofMarkedGroup a = ofMarkedGroup b ↔ a = b := .rfl - -variable (α : Type*) - -@[to_additive] -instance MarkedGroup.instInhabited [Inhabited G] : Inhabited (MarkedGroup m) := ‹Inhabited G› - -@[to_additive] -instance MarkedGroup.instSmul [SMul G α] : SMul (MarkedGroup m) α := ‹SMul G α› - -@[to_additive] -instance MarkedGroup.instMulAction [MulAction G α] : MulAction (MarkedGroup m) α := ‹MulAction G α› - -@[to_additive (attr := simp)] -lemma toMarkedGroup_smul (g : G) (x : α) [SMul G α] : - (toMarkedGroup g : MarkedGroup m) • x = g • x := rfl - -@[to_additive (attr := simp)] -lemma ofMarkedGroup_smul (g : MarkedGroup m) (x : α) [SMul G α] : ofMarkedGroup g • x = g • x := rfl - -@[to_additive] -private lemma mul_aux [DecidableEq S] (x : MarkedGroup m) : - ∃ (n : _) (l : FreeGroup S), toMarkedGroup (m l) = x ∧ l.toWord.length ≤ n := by - classical - obtain ⟨l, rfl⟩ := m.coe_surjective x - exact ⟨_, _, rfl, le_rfl⟩ - -@[to_additive] -private lemma mul_aux' [DecidableEq S] (x : MarkedGroup m) : - ∃ (n : _) (l : FreeGroup S), toMarkedGroup (m l) = x ∧ l.toWord.length = n := by - classical - obtain ⟨l, rfl⟩ := m.coe_surjective x - exact ⟨_, _, rfl, rfl⟩ - -@[to_additive] -private lemma find_mul_aux [DecidableEq S] (x : MarkedGroup m) - [DecidablePred fun n ↦ ∃ l, toMarkedGroup (m l) = x ∧ l.toWord.length ≤ n] - [DecidablePred fun n ↦ ∃ l, toMarkedGroup (m l) = x ∧ l.toWord.length = n] : - Nat.find (mul_aux x) = Nat.find (mul_aux' x) := by - classical - exact _root_.le_antisymm (Nat.find_mono fun n => Exists.imp fun l => And.imp_right le_of_eq) <| - (Nat.le_find_iff _ _).2 fun k hk ⟨l, hl, hlk⟩ => (Nat.lt_find_iff _ _).1 hk _ hlk ⟨l, hl, rfl⟩ - -@[to_additive] -noncomputable instance : NormedGroup (MarkedGroup m) := - GroupNorm.toNormedGroup - { toFun := fun x => by classical exact (Nat.find (mul_aux x)).cast - map_one' := by - classical - exact cast_eq_zero.2 <| (find_eq_zero <| mul_aux _).2 ⟨1, by simp_rw [map_one], le_rfl⟩ - mul_le' := fun x y => by - classical - dsimp - norm_cast - obtain ⟨a, rfl, ha⟩ := Nat.find_spec (mul_aux x) - obtain ⟨b, rfl, hb⟩ := Nat.find_spec (mul_aux y) - refine find_le ⟨a * b, by simp, (a.toWord_mul_sublist _).length_le.trans ?_⟩ - rw [length_append] - gcongr - inv' := by - classical - suffices ∀ {x : MarkedGroup m}, Nat.find (mul_aux x⁻¹) ≤ Nat.find (mul_aux x) by - dsimp - refine fun _ => congr_arg Nat.cast (this.antisymm ?_) - convert this - simp_rw [inv_inv] - rintro x - refine find_mono fun nI => ?_ - rintro ⟨l, hl, h⟩ - exact ⟨l⁻¹, by simp [hl], h.trans_eq' <| by simp⟩ - eq_one_of_map_eq_zero' := fun x hx => by - classical - obtain ⟨l, rfl, hl⟩ := (find_eq_zero <| mul_aux _).1 (cast_eq_zero.1 hx) - rw [le_zero_iff, length_eq_zero, ← FreeGroup.toWord_one] at hl - rw [FreeGroup.toWord_injective hl, map_one, map_one] } - -@[to_additive] -instance : DiscreteTopology (MarkedGroup (GroupMarking.refl : GroupMarking G G)) := - sorry - -namespace MarkedGroup - -@[to_additive] -lemma norm_def [DecidableEq S] (x : MarkedGroup m) - [DecidablePred fun n ↦ ∃ l, toMarkedGroup (m l) = x ∧ l.toWord.length = n] : - ‖x‖ = Nat.find (mul_aux' x) := by - convert congr_arg Nat.cast (find_mul_aux _) - classical - infer_instance - -@[to_additive (attr := simp)] -lemma norm_eq_one (x : MarkedGroup m) : - ‖x‖ = 1 ↔ ∃ s, toMarkedGroup (m <| FreeGroup.mk [s]) = x := by - classical - simp_rw [norm_def, Nat.cast_eq_one, Nat.find_eq_iff, length_eq_one] - constructor - · rintro ⟨⟨l, rfl, s, hl⟩, hn⟩ - refine ⟨s, ?_⟩ - rw [← hl, FreeGroup.mk_toWord] - rintro ⟨s, rfl⟩ - refine ⟨⟨_, rfl, s, ?_⟩, ?_⟩ - simp only [FreeGroup.toWord_mk, FreeGroup.reduce_singleton] - sorry - -@[simp] -lemma norm_toMarkedGroup (s : S) : ‖(toMarkedGroup (m (FreeGroup.of s)) : MarkedGroup m)‖ = 1 := - sorry - -lemma gen_set_mul_right (x : MarkedGroup m) (s : S) : - ‖(toMarkedGroup (ofMarkedGroup x * m (FreeGroup.of s)) : MarkedGroup m)‖ ≤ ‖x‖ + 1 := - sorry - -lemma gen_set_mul_right' (x : MarkedGroup m) {n : ℝ} (hx : ‖x‖ ≤ n) (s : S) : - ‖(toMarkedGroup (ofMarkedGroup x * m (FreeGroup.of s)) : MarkedGroup m)‖ ≤ n + 1 := - sorry - -lemma gen_set_mul_left (x : MarkedGroup m) (s : S) : - ‖(toMarkedGroup (m (FreeGroup.of s) * ofMarkedGroup x) : MarkedGroup m)‖ ≤ ‖x‖ + 1 := - sorry - -lemma gen_set_mul_left' (x : MarkedGroup m) {n : ℝ} (hx : ‖x‖ ≤ n) (s : S) : - ‖(toMarkedGroup (m (FreeGroup.of s) * ofMarkedGroup x) : MarkedGroup m)‖ ≤ n + 1 := - sorry - -lemma dist_one_iff (x y : MarkedGroup m) : - dist x y = 1 ↔ (∃ s : S, x * toMarkedGroup (m (.of s)) = y) ∨ - ∃ s : S, y * toMarkedGroup (m (.of s)) = x := - sorry - -lemma gen_set_div (x : MarkedGroup m) (hx : x ≠ 1) : - ∃ y : MarkedGroup m, dist x y = 1 ∧ ‖y‖ = ‖x‖ - 1 := - sorry - -lemma gen_div_left (x : MarkedGroup m) (hx : x ≠ 1) : - ∃ y : MarkedGroup m, - ((∃ s : S, toMarkedGroup (m (.of s)) * y = x) ∨ - ∃ s : S, toMarkedGroup (m (.of s)⁻¹) * y = x) ∧ ‖y‖ = ‖x‖ - 1 := - sorry - --- same lemmas but for subsets -lemma gen_norm_le_one_sub {H : Set G} {m' : GroupMarking G H} {s : MarkedGroup m'} (sh : s ∈ H) : - ‖s‖ ≤ 1 := - sorry - -lemma gen_set_mul_right_sub {H : Set G} {s : G} {m' : GroupMarking G H} (sh : s ∈ H) - (g : MarkedGroup m') : ‖g * toMarkedGroup s‖ ≤ ‖g‖ + 1 := - sorry - -lemma gen_set_mul_right'_sub {H : Set G} {s : G} {m' : GroupMarking G H} (sh : s ∈ H) - (g : MarkedGroup m') {n : ℝ} (hg : ‖g‖ ≤ n) : ‖g * toMarkedGroup s‖ ≤ n + 1 := - sorry - -lemma gen_set_mul_left_sub {H : Set G} {m' : GroupMarking G H} (g s : MarkedGroup m') - (sh : s ∈ H) : ‖s * g‖ ≤ ‖g‖ + 1 := - sorry - -lemma gen_set_mul_left'_sub {H : Set G} {m' : GroupMarking G H} (g s : MarkedGroup m') - (sh : s ∈ H) {n : ℝ} (hg : ‖g‖ ≤ n) : ‖s * g‖ ≤ n + 1 := - sorry - -lemma dist_one_iff_sub {H : Set G} {m' : GroupMarking G H} (x y : MarkedGroup m') : - dist x y = 1 ↔ (∃ s ∈ H, x * toMarkedGroup s = y) ∨ ∃ s ∈ H, y * toMarkedGroup s = x := - sorry - -lemma gen_div_left_sub {H : Set G} {m' : GroupMarking G H} (x : MarkedGroup m') (hx : x ≠ 1) : - ∃ y : MarkedGroup m', ((∃ s ∈ H, toMarkedGroup s * y = x) ∨ - ∃ s ∈ H, (toMarkedGroup s)⁻¹ * y = x) ∧ ‖y‖ = ‖x‖ - 1 := - sorry - -end MarkedGroup diff --git a/LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean b/LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean deleted file mode 100644 index 825ef6bc08..0000000000 --- a/LeanCamCombi/GrowthInGroups/ApproximateSubgroup.lean +++ /dev/null @@ -1,210 +0,0 @@ -import Mathlib.Algebra.Group.Subgroup.Pointwise -import Mathlib.Algebra.Order.BigOperators.Ring.Finset -import Mathlib.Combinatorics.Additive.CovBySMul -import Mathlib.Combinatorics.Additive.RuzsaCovering -import Mathlib.Combinatorics.Additive.SmallTripling -import Mathlib.Combinatorics.Additive.VerySmallDoubling -import Mathlib.Tactic.Bound - --- TODO: Unsimp in mathlib -attribute [-simp] Set.image_subset_iff - -open scoped Finset Pointwise - -variable {G : Type*} [Group G] {A B : Set G} {K L : ℝ} {m n : ℕ} - -structure IsApproximateAddSubgroup {G : Type*} [AddGroup G] (K : ℝ) (A : Set G) : Prop where - zero_mem : 0 ∈ A - neg_eq_self : -A = A - two_nsmul_covByVAdd : CovByVAdd G K (2 • A) A - -@[to_additive] -structure IsApproximateSubgroup (K : ℝ) (A : Set G) : Prop where - one_mem : 1 ∈ A - inv_eq_self : A⁻¹ = A - sq_covBySMul : CovBySMul G K (A ^ 2) A - -namespace IsApproximateSubgroup - -@[to_additive] -lemma nonempty (hA : IsApproximateSubgroup K A) : A.Nonempty := ⟨1, hA.one_mem⟩ - -@[to_additive one_le] -lemma one_le (hA : IsApproximateSubgroup K A) : 1 ≤ K := by - obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul - have hF₀ : F ≠ ∅ := by rintro rfl; simp [hA.nonempty.pow.ne_empty] at hSF - exact hF.trans' <| by simpa [Finset.nonempty_iff_ne_empty] - -@[to_additive] -lemma mono (hKL : K ≤ L) (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup L A where - one_mem := hA.one_mem - inv_eq_self := hA.inv_eq_self - sq_covBySMul := hA.sq_covBySMul.mono hKL - -@[to_additive] -lemma card_pow_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) : - ∀ {n}, #(A ^ n) ≤ K ^ (n - 1) * #A - | 0 => by simpa using hA.nonempty - | 1 => by simp - | n + 2 => by - obtain ⟨F, hF, hSF⟩ := hA.sq_covBySMul - calc - (#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A) := by - gcongr; exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by omega) - _ ≤ #(F ^ (n + 1)) * #A := mod_cast Finset.card_mul_le - _ ≤ #F ^ (n + 1) * #A := by gcongr; exact mod_cast Finset.card_pow_le - _ ≤ K ^ (n + 1) * #A := by gcongr - -@[to_additive] -lemma card_mul_self_le [DecidableEq G] {A : Finset G} (hA : IsApproximateSubgroup K (A : Set G)) : - #(A * A) ≤ K * #A := by simpa [sq] using hA.card_pow_le (n := 2) - -@[to_additive] -lemma image {F H : Type*} [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F) - (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup K (f '' A) where - one_mem := ⟨1, hA.one_mem, map_one _⟩ - inv_eq_self := by simp [← Set.image_inv, hA.inv_eq_self] - sq_covBySMul := by - classical - obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul - refine ⟨F.image f, ?_, ?_⟩ - · calc - (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le - _ ≤ K := hF - · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢ - gcongr - -@[to_additive] -lemma pi {ι : Type*} {G : ι → Type*} [Fintype ι] [∀ i, Group (G i)] {A : ∀ i, Set (G i)} {K : ι → ℝ} - (hA : ∀ i, IsApproximateSubgroup (K i) (A i)) : - IsApproximateSubgroup (∏ i, K i) (Set.univ.pi A) where - one_mem i _ := (hA i).one_mem - inv_eq_self := by simp [(hA _).inv_eq_self] - sq_covBySMul := by - choose F hF hFS using fun i ↦ (hA i).sq_covBySMul - classical - refine ⟨Fintype.piFinset F, ?_, ?_⟩ - · calc - #(Fintype.piFinset F) = ∏ i, (#(F i) : ℝ) := by simp - _ ≤ ∏ i, K i := by gcongr; exact hF _ - · sorry - -@[to_additive] -lemma subgroup {S : Type*} [SetLike S G] [SubgroupClass S G] {H : S} : - IsApproximateSubgroup 1 (H : Set G) where - one_mem := OneMemClass.one_mem H - inv_eq_self := inv_coe_set - sq_covBySMul := ⟨{1}, by simp⟩ - -open Finset in -@[to_additive] -lemma of_small_tripling [DecidableEq G] {A : Finset G} (hA₁ : 1 ∈ A) (hAsymm : A⁻¹ = A) - (hA : #(A ^ 3) ≤ K * #A) : IsApproximateSubgroup (K ^ 3) (A ^ 2 : Set G) where - one_mem := by rw [sq, ← one_mul 1]; exact Set.mul_mem_mul hA₁ hA₁ - inv_eq_self := by simp [← inv_pow, hAsymm, ← coe_inv] - sq_covBySMul := by - replace hA := calc (#(A ^ 4 * A) : ℝ) - _ = #(A ^ 5) := by rw [← pow_succ] - _ ≤ K ^ 3 * #A := small_pow_of_small_tripling' (by omega) hA hAsymm - have hA₀ : A.Nonempty := ⟨1, hA₁⟩ - obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA - have hF₀ : F.Nonempty := nonempty_iff_ne_empty.2 <| by rintro rfl; simp [hA₀.ne_empty] at hAF - exact ⟨F, hF, by norm_cast; simpa [div_eq_mul_inv, pow_succ, mul_assoc, hAsymm] using hAF⟩ - -open Set in -@[to_additive] -lemma pow_inter_pow_covBySMul_sq_inter_sq - (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m) (hn : 2 ≤ n) : - CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2) := by - classical - obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul - obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul - have := hA.one_le - choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B - refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩ - · calc - (#(.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : ℝ) - _ ≤ #(F₁ ^ (m - 1)) * #(F₂ ^ (n - 1)) := mod_cast Finset.card_image₂_le .. - _ ≤ #F₁ ^ (m - 1) * #F₂ ^ (n - 1) := by gcongr <;> exact mod_cast Finset.card_pow_le - _ ≤ K ^ (m - 1) * L ^ (n - 1) := by gcongr - · calc - A ^ m ∩ B ^ n ⊆ (F₁ ^ (m - 1) * A) ∩ (F₂ ^ (n - 1) * B) := by - gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> omega - _ = ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), a • A ∩ b • B := by - simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]; norm_cast - _ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) := by - gcongr; exact hf .. - _ = (Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2) := by - simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq] - rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2] - simp_rw [Finset.mem_coe] - -open Set in -@[to_additive] -lemma pow_inter_pow (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m) - (hn : 2 ≤ n) : - IsApproximateSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (A ^ m ∩ B ^ n) where - one_mem := ⟨Set.one_mem_pow hA.one_mem, Set.one_mem_pow hB.one_mem⟩ - inv_eq_self := by simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self] - sq_covBySMul := by - refine (hA.pow_inter_pow_covBySMul_sq_inter_sq hB (by omega) (by omega)).subset ?_ - (by gcongr; exacts [hA.one_mem, hB.one_mem]) - calc - (A ^ m ∩ B ^ n) ^ 2 ⊆ (A ^ m) ^ 2 ∩ (B ^ n) ^ 2 := Set.inter_pow_subset - _ = A ^ (2 * m) ∩ B ^ (2 * n) := by simp [pow_mul'] - -end IsApproximateSubgroup - -open MulAction in -/-- A finite `1`-approximate subgroup is the same thing as a finite subgroup. - -Note that various sources claim this with no proof, some of them without the necessary assumptions -to make it true (eg Wikipedia before I fixed it). -/ -@[to_additive (attr := simp) -"A finite `1`-approximate subgroup is the same thing as a finite subgroup. - -Note that various sources claim this with no proof, some of them without the necessary assumptions -to make it true (eg Wikipedia before I fixed it)."] -lemma isApproximateSubgroup_one {S : Type*} [SetLike S G] [SubgroupClass S G] {A : Set G} - (hA : A.Finite) : - IsApproximateSubgroup 1 (A : Set G) ↔ ∃ H : Subgroup G, H = A where - mp hA' := by - classical - lift A to Finset G using hA - exact ⟨stabilizer G A, by simpa using - Finset.smul_stabilizer_of_no_doubling (by simpa using hA'.card_mul_self_le) hA'.one_mem⟩ - mpr := by rintro ⟨H, rfl⟩; exact .subgroup - -open Finset in -open scoped RightActions in -@[to_additive] -lemma exists_isApproximateSubgroup_of_small_doubling [DecidableEq G] {A : Finset G} - (hA₀ : A.Nonempty) (hA : #(A ^ 2) ≤ K * #A) : - ∃ S ⊆ (A⁻¹ * A) ^ 2, IsApproximateSubgroup (2 ^ 12 * K ^ 36) (S : Set G) ∧ - #S ≤ 16 * K ^ 12 * #A ∧ ∃ a ∈ A, #A / (2 * K) ≤ #(A ∩ S <• a) := by - have hK : 1 ≤ K := one_le_of_le_mul_right₀ (by positivity) <| - calc (#A : ℝ) ≤ #(A ^ 2) := mod_cast card_le_card_pow two_ne_zero - _ ≤ K * #A := hA - let S : Finset G := {g ∈ A⁻¹ * A | #A / (2 * K) ≤ #(A <• g ∩ A)} - have hS₁ : 1 ∈ S := by simp [S, hA₀.ne_empty]; bound - have hS₀ : S.Nonempty := ⟨1, hS₁⟩ - have hSA : S ⊆ A⁻¹ * A := filter_subset .. - have hSsymm : S⁻¹ = S := by ext; simp [S]; simp [← mem_inv']; sorry - have hScard := calc - (#S : ℝ) ≤ #(A⁻¹ * A) := by gcongr - _ ≤ K ^ 2 * #A := sorry - obtain ⟨F, hFA, hFcard, hASF⟩ : ∃ F ⊆ A, #F ≤ 2 * K ∧ A ⊆ S * F := sorry - refine ⟨S ^ 2, by gcongr, ?_, ?_, ?_⟩ - · rw [show 2 ^ 12 * K ^ 36 = (2 ^ 4 * K ^ 12) ^ 3 by ring, coe_pow] - refine .of_small_tripling hS₁ hSsymm ?_ - calc - (#(S ^ 3) : ℝ) - _ ≤ #(A * S ^ 3) := mod_cast card_le_card_mul_left hA₀ - _ ≤ #(A * S ^ 3 * A⁻¹) := mod_cast card_le_card_mul_right hA₀.inv - _ ≤ 8 * K ^ 11 * #A := sorry - _ ≤ 8 * K ^ 11 * #(S * F) := by gcongr - _ ≤ 8 * K ^ 11 * (#S * #F) := by gcongr; exact mod_cast card_mul_le - _ ≤ 8 * K ^ 11 * (#S * (2 * K)) := by gcongr - _ = 2 ^ 4 * K ^ 12 * #S := by ring - sorry - sorry diff --git a/LeanCamCombi/GrowthInGroups/Chevalley.lean b/LeanCamCombi/GrowthInGroups/Chevalley.lean deleted file mode 100644 index d1da3e7a1f..0000000000 --- a/LeanCamCombi/GrowthInGroups/Chevalley.lean +++ /dev/null @@ -1,241 +0,0 @@ -import Mathlib.Data.DFinsupp.WellFounded -import Mathlib.RingTheory.Localization.Algebra -import Mathlib.RingTheory.Spectrum.Prime.Polynomial -import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum - -open Polynomial PrimeSpectrum TensorProduct Topology - -universe u v -variable {R M A} [CommRing R] [AddCommGroup M] [Module R M] [CommRing A] [Algebra R A] - -lemma Ideal.span_range_update_divByMonic' {ι : Type*} [DecidableEq ι] - (v : ι → R[X]) (i j : ι) (hij : i ≠ j) (h : IsUnit (v i).leadingCoeff) : - Ideal.span (Set.range (Function.update v j (v j %ₘ (C ((h.unit⁻¹ : Rˣ) : R) * v i)))) = - Ideal.span (Set.range v) := by - have H : (C (↑(h.unit⁻¹) : R) * v i).Monic := by simp [Monic, leadingCoeff_C_mul_of_isUnit] - refine le_antisymm ?_ ?_ <;> - simp only [Ideal.span_le, Set.range_subset_iff, SetLike.mem_coe] - · intro k - by_cases hjk : j = k - · subst hjk - rw [Function.update_self, modByMonic_eq_sub_mul_div (v j) H] - apply sub_mem (Ideal.subset_span ?_) (Ideal.mul_mem_right _ _ - (Ideal.mul_mem_left _ _ <| Ideal.subset_span ?_)) - · exact ⟨j, rfl⟩ - · exact ⟨i, rfl⟩ - exact Ideal.subset_span ⟨k, (Function.update_of_ne (.symm hjk) _ _).symm⟩ - · intro k - by_cases hjk : j = k - · subst hjk - nth_rw 2 [← modByMonic_add_div (v j) H] - apply add_mem (Ideal.subset_span ?_) (Ideal.mul_mem_right _ _ - (Ideal.mul_mem_left _ _ <| Ideal.subset_span ?_)) - · exact ⟨j, Function.update_self _ _ _⟩ - · exact ⟨i, Function.update_of_ne hij _ _⟩ - exact Ideal.subset_span ⟨k, Function.update_of_ne (.symm hjk) _ _⟩ - -lemma foo_induction - (P : ∀ (R : Type u) [CommRing R], Ideal R[X] → Prop) - (hP₀ : ∀ (R) [CommRing R] (g : R[X]), g.Monic → P R (Ideal.span {g})) - (hP₁ : ∀ (R) [CommRing R], P R ⊥) - (hP : ∀ (R) [CommRing R] (c : R) (I : Ideal R[X]), - P (Localization.Away c) (I.map (mapRingHom (algebraMap _ _))) → - P (R ⧸ Ideal.span {c}) (I.map (mapRingHom (algebraMap _ _))) → P R I) - {R} [CommRing R] (I : Ideal R[X]) (hI : I.FG) : P R I := by - classical - obtain ⟨n, e, rfl⟩ : ∃ (n : ℕ) (e : Fin (n + 1) → R[X]), I = Ideal.span (Set.range e) := by - obtain ⟨s, rfl⟩ := hI - exact ⟨s.card, Fin.cons 0 (Subtype.val ∘ s.equivFin.symm), - by simp [← Set.union_singleton, Ideal.span_union, Set.singleton_zero]⟩ - clear hI - set v : (Fin (n + 1) → WithBot ℕ) ×ₗ Prop := toLex - (degree ∘ e, ¬ ∃ i, IsUnit (e i).leadingCoeff ∧ ∀ j, e j ≠ 0 → - (e i).degree ≤ (e j).degree) with hv - clear_value v - induction' v using WellFoundedLT.induction with v H_IH generalizing R - by_cases he0 : e = 0 - · simpa [he0, Set.range_zero, Set.singleton_zero] using hP₁ R - cases subsingleton_or_nontrivial R - · rw [Subsingleton.elim (Ideal.span (Set.range e)) ⊥]; exact hP₁ R - simp only [funext_iff, Pi.zero_apply, not_forall] at he0 - -- Case I : The `e i ≠ 0` with minimal degree has invertible leading coefficient - by_cases H : ∃ i, IsUnit (e i).leadingCoeff ∧ ∀ j, e j ≠ 0 → (e i).degree ≤ (e j).degree - · obtain ⟨i, hi, i_min⟩ := H - have hi_monic : (C (↑(hi.unit⁻¹) : R) * e i).Monic := by simp [Monic, leadingCoeff_C_mul_of_isUnit] - -- Case I.ii : `e j = 0` for all `j ≠ i`. - by_cases H' : ∀ j ≠ i, e j = 0 - -- then `I = Ideal.span {e i}` - · convert hP₀ R (C ((hi.unit⁻¹ : Rˣ) : R) * e i) hi_monic using 1 - refine le_antisymm ?_ ?_ <;> - simp only [Ideal.span_le, Set.range_subset_iff, Set.singleton_subset_iff] - · intro j - by_cases hij : i = j - · simp only [SetLike.mem_coe, Ideal.mem_span_singleton] - use C (e i).leadingCoeff - rw [mul_comm, ← mul_assoc, ← map_mul, IsUnit.mul_val_inv, map_one, one_mul, hij] - · rw [H' j (.symm hij)] - exact Ideal.zero_mem _ - · exact Ideal.mul_mem_left _ _ (Ideal.subset_span (Set.mem_range_self i)) - -- Case I.i : There is another `e j ≠ 0` - · simp only [ne_eq, not_forall, Classical.not_imp] at H' - obtain ⟨j, hj, hj'⟩ := H' - replace i_min := i_min j hj' - -- then we can replace `e j` with `e j %ₘ (C h.unit⁻¹ * e i) ` - -- with `h : IsUnit (e i).leadingCoeff`. - rw [← Ideal.span_range_update_divByMonic' e i j (.symm hj) hi] - refine H_IH _ ?_ _ rfl - refine .left _ _ (lt_of_le_of_ne (b := (ofLex v).1) ?_ ?_) - · intro k - simp only [Function.comp_apply, Function.update_apply, hv, ne_eq, not_exists, not_and, - not_forall, Classical.not_imp, not_le, ofLex_toLex] - split_ifs with hjk - · rw [hjk] - refine (degree_modByMonic_le _ hi_monic).trans - ((degree_C_mul_of_mul_ne_zero ?_).trans_le i_min) - rw [IsUnit.val_inv_mul] - exact one_ne_zero - · exact le_rfl - · simp only [hv, ne_eq, not_exists, not_and, not_forall, not_le, funext_iff, - Function.comp_apply, exists_prop, ofLex_toLex] - use j - simp only [Function.update_self] - refine ((degree_modByMonic_lt _ hi_monic).trans_le <| - (degree_C_mul_of_mul_ne_zero ?_).trans_le i_min).ne - rw [IsUnit.val_inv_mul] - exact one_ne_zero - -- Case II : The `e i ≠ 0` with minimal degree has non-invertible leading coefficient - obtain ⟨i, hi, i_min⟩ : ∃ i, e i ≠ 0 ∧ ∀ j, e j ≠ 0 → (e i).degree ≤ (e j).degree := by - have : ∃ n : ℕ, ∃ i, (e i).degree = n ∧ (e i) ≠ 0 := by - obtain ⟨i, hi⟩ := he0; exact ⟨(e i).natDegree, i, degree_eq_natDegree hi, hi⟩ - let m := Nat.find this - obtain ⟨i, hi, hi'⟩ : ∃ i, (e i).degree = m ∧ (e i) ≠ 0 := Nat.find_spec this - refine ⟨i, hi', fun j hj ↦ ?_⟩ - refine hi.le.trans ?_ - rw [degree_eq_natDegree hj, Nat.cast_le] - exact Nat.find_min' _ ⟨j, degree_eq_natDegree hj, hj⟩ - have : ¬ IsUnit (e i).leadingCoeff := fun HH ↦ H ⟨i, HH, i_min⟩ - -- We replace `R` by `R ⧸ Ideal.span {(e i).leadingCoeff}` where `(e i).degree` is lowered - -- and `Localization.Away (e i).leadingCoeff` where `(e i).leadingCoeff` becomes invertible. - apply hP _ (e i).leadingCoeff - · rw [Ideal.map_span, ← Set.range_comp] - refine H_IH _ ?_ _ rfl - rw [hv, Prod.Lex.lt_iff'] - constructor - · intro j; simpa using degree_map_le - simp only [coe_mapRingHom, Function.comp_apply, ne_eq, hv, ofLex_toLex, - not_exists, not_and, not_forall, Classical.not_imp, not_le, H, not_false_eq_true] - intro h_eq - rw [lt_iff_le_not_le] - simp only [exists_prop, le_Prop_eq, implies_true, true_implies, not_forall, Classical.not_imp, - not_exists, not_and, not_lt, true_and] - refine ⟨i, ?_, ?_⟩ - · replace h_eq := congr_fun h_eq i - simp only [Function.comp_apply] at h_eq - have := IsLocalization.Away.algebraMap_isUnit (S := Localization.Away (e i).leadingCoeff) - (e i).leadingCoeff - convert this - nth_rw 2 [← coeff_natDegree] - rw [natDegree_eq_of_degree_eq h_eq, coeff_map, coeff_natDegree] - · intro j hj - refine le_trans ?_ ((i_min j (fun e ↦ hj (by simp [e]))).trans_eq (congr_fun h_eq j).symm) - simpa using degree_map_le - · rw [Ideal.map_span, ← Set.range_comp] - refine H_IH _ ?_ _ rfl - rw [hv] - refine .left _ _ (lt_of_le_of_ne ?_ ?_) - · intro j; simpa using degree_map_le - simp only [coe_mapRingHom, Function.comp_apply, ne_eq, hv, ofLex_toLex, - not_exists, not_and, not_forall, Classical.not_imp, not_le, H, not_false_eq_true] - intro h_eq - replace h_eq := congr_fun h_eq i - simp only [Ideal.Quotient.algebraMap_eq, Function.comp_apply, degree_map_eq_iff, - Ideal.Quotient.mk_singleton_self, ne_eq, not_true_eq_false, false_or] at h_eq - exact hi h_eq - -lemma comap_C_eq_comap_quotient_union_comap_localization (s : Set (PrimeSpectrum R[X])) (c : R) : - 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 '' - (comap (mapRingHom (algebraMap R (Localization.Away c))) ⁻¹' s)) := by - simp_rw [← Set.image_comp, ← ContinuousMap.coe_comp, ← comap_comp, ← mapRingHom_comp_C, - comap_comp, ContinuousMap.coe_comp, Set.image_comp, Set.image_preimage_eq_inter_range, - ← Set.image_union, ← Set.inter_union_distrib_left] - letI := (mapRingHom (algebraMap R (Localization.Away c))).toAlgebra - suffices Set.range (comap (mapRingHom (Ideal.Quotient.mk (.span {c})))) = - (Set.range (comap (algebraMap R[X] (Localization.Away c)[X])))ᶜ by - rw [this, RingHom.algebraMap_toAlgebra, Set.compl_union_self, Set.inter_univ] - have := Polynomial.isLocalization (.powers c) (Localization.Away c) - rw [Submonoid.map_powers] at this - have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span {c}))) := - Polynomial.map_surjective _ Ideal.Quotient.mk_surjective - rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)] - simp [Polynomial.ker_mapRingHom, Ideal.map_span] - -lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus {R} [CommRing R] - (I : Ideal R[X]) (hI : I.FG) (f : R[X]) : - IsConstructible (comap C '' (zeroLocus I \ zeroLocus {f})) := by - revert f - apply foo_induction (hI := hI) - · intros R _ g hg f - simp only [zeroLocus_span] - exact ((isRetrocompact_iff (isOpen_image_comap_of_monic f g hg)).mpr - (isCompact_image_comap_of_monic f g hg)).isConstructible (isOpen_image_comap_of_monic f g hg) - · intro R _ f - simp only [Submodule.bot_coe, zeroLocus_singleton_zero, ← Set.compl_eq_univ_diff, - ← basicOpen_eq_zeroLocus_compl] - exact ((isRetrocompact_iff (isOpenMap_comap_C _ (basicOpen f).2)).mpr - ((isCompact_basicOpen f).image (comap C).2)).isConstructible - (isOpenMap_comap_C _ (basicOpen f).2) - · intro R _ c I H₁ H₂ f - replace H₁ := (H₁ (mapRingHom (algebraMap _ _) f)).image_of_isOpenEmbedding - (localization_away_isOpenEmbedding (Localization.Away c) c) - (by rw [localization_away_comap_range _ c] - exact (isRetrocompact_iff (basicOpen c).2).mpr (isCompact_basicOpen c)) - replace H₂ := (H₂ (mapRingHom (Ideal.Quotient.mk _) f)).image_of_isClosedEmbedding - (isClosedEmbedding_comap_of_surjective _ _ Ideal.Quotient.mk_surjective) - (by rw [range_comap_of_surjective _ _ Ideal.Quotient.mk_surjective] - simp only [Ideal.mk_ker, zeroLocus_span, ← basicOpen_eq_zeroLocus_compl] - exact (isRetrocompact_iff (basicOpen c).2).mpr (isCompact_basicOpen c)) - rw [comap_C_eq_comap_quotient_union_comap_localization _ c] - simp_rw [Set.preimage_diff, preimage_comap_zeroLocus, Set.image_singleton] - convert H₂.union H₁ using 5 <;> - simp only [Ideal.map, zeroLocus_span, coe_mapRingHom, Ideal.Quotient.algebraMap_eq] - -lemma isConstructible_image_comap_C {R} [CommRing R] (s : Set (PrimeSpectrum R[X])) - (hs : IsConstructible s) : - IsConstructible (comap C '' s) := by - induction s, hs using IsConstructible.induction_of_isTopologicalBasis (ι := R[X]) _ - isTopologicalBasis_basic_opens with - | compact_inter i j => - rw [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul] - exact isCompact_basicOpen _ - | union s hs t ht hs' ht' => - rw [Set.image_union] - exact hs'.union ht' - | sdiff i s hs => - simp only [basicOpen_eq_zeroLocus_compl, ← Set.compl_iInter₂, - compl_sdiff_compl, ← zeroLocus_iUnion₂, Set.biUnion_of_singleton] - rw [← zeroLocus_span] - apply isConstructible_comap_C_zeroLocus_sdiff_zeroLocus - exact ⟨hs.toFinset, by simp⟩ - -lemma isConstructible_image_comap {R S} [CommRing R] [CommRing S] (f : R →+* S) - (hf : RingHom.FinitePresentation f) - (s : Set (PrimeSpectrum S)) (hs : IsConstructible s) : - IsConstructible (comap f '' s) := by - apply hf.polynomial_induction - (P := fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s)) - (Q := fun _ _ _ _ f ↦ ∀ s, IsConstructible s → IsConstructible (comap f '' s)) - · exact fun _ ↦ isConstructible_image_comap_C - · intro R _ S _ f hf hf' s hs - refine hs.image_of_isClosedEmbedding (isClosedEmbedding_comap_of_surjective _ _ hf) ?_ - rw [range_comap_of_surjective _ _ hf, isRetrocompact_iff (isClosed_zeroLocus _).isOpen_compl] - obtain ⟨t, ht⟩ := hf' - rw [← ht, ← t.toSet.iUnion_of_singleton_coe, zeroLocus_span, zeroLocus_iUnion, Set.compl_iInter] - apply isCompact_iUnion - exact fun _ ↦ by simpa using isCompact_basicOpen _ - · intro R _ S _ T _ f g hf hg s hs - simp only [comap_comp, ContinuousMap.coe_comp, Set.image_comp] - exact hf _ (hg _ hs) - · exact hs diff --git a/LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean b/LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean index 27171d6b5a..b45ca6bf11 100644 --- a/LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean +++ b/LeanCamCombi/GrowthInGroups/ChevalleyComplex.lean @@ -1,18 +1,14 @@ import Mathlib.Algebra.Order.SuccPred.WithBot import Mathlib.Algebra.Polynomial.CoeffMem import Mathlib.Data.DFinsupp.WellFounded +import Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet import Mathlib.RingTheory.Spectrum.Prime.Polynomial -import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Basic import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Degrees -import LeanCamCombi.Mathlib.Algebra.MvPolynomial.Equiv -import LeanCamCombi.Mathlib.Data.Set.Image -import LeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.Topology -import LeanCamCombi.GrowthInGroups.ConstructibleSetData variable {R S M A : Type*} [CommRing R] [CommRing S] [AddCommGroup M] [Module R M] [CommRing A] [Algebra R A] -open Function Localization Polynomial TensorProduct PrimeSpectrum +open Function Localization MvPolynomial Polynomial TensorProduct PrimeSpectrum open scoped Pointwise variable (R) in @@ -74,10 +70,10 @@ lemma powBound_ne_zero : e.powBound ≠ 0 := by attribute [-instance] Ring.toIntAlgebra in variable (R n e) in def InductionStatement [Algebra ℤ R] : Prop := - ∀ f, ∃ T : Finset (Σ n, R × (Fin n → R)), - 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 ≤ e.degBound ∧ ∀ i, C.2.2 i ∈ e.coeffSubmodule ^ e.powBound + ∀ f, ∃ T : Finset (R × Σ n, Fin n → R), + comap Polynomial.C '' (zeroLocus (Set.range e.val) \ zeroLocus {f}) = + ⋃ C ∈ T, (zeroLocus (Set.range C.2.2) \ zeroLocus {C.1}) ∧ + ∀ C ∈ T, C.2.1 ≤ e.degBound ∧ ∀ i, C.2.2 i ∈ e.coeffSubmodule ^ e.powBound local notation3 "coeff("p")" => Set.range (Polynomial.coeff p) @@ -93,7 +89,7 @@ lemma foo_induction (n : ℕ) P R ⟨Function.update e.1 j (e.1 j %ₘ e.1 i)⟩ → P R e) (hP : ∀ (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n), c = (e.1 i).leadingCoeff → c ≠ 0 → - P (Away c) ⟨C (IsLocalization.Away.invSelf (S := Away c) c) • + P (Away c) ⟨Polynomial.C (IsLocalization.Away.invSelf (S := Away c) c) • mapRingHom (algebraMap _ _) ∘ e.val⟩ → P (R ⧸ Ideal.span {c}) ⟨mapRingHom (algebraMap _ _) ∘ e.val⟩ → P R e) {R} [CommRing R] (e : InductionObj R n) : P R e := by @@ -164,7 +160,8 @@ lemma foo_induction (n : ℕ) intro h_eq refine ⟨i, ?_, ?_⟩ · rw [Monic.def, ← coeff_natDegree (p := _ * _), natDegree_eq_of_degree_eq (h_eq i), - coeff_C_mul, coeff_map, coeff_natDegree, mul_comm, IsLocalization.Away.mul_invSelf] + Polynomial.coeff_C_mul, Polynomial.coeff_map, coeff_natDegree, mul_comm, + IsLocalization.Away.mul_invSelf] · intro j hj; rw [h_eq, h_eq]; exact i_min j fun H ↦ (by simp [H] at hj) · rw [hv] refine .left _ _ (lt_of_le_of_ne ?_ ?_) @@ -185,7 +182,7 @@ open Submodule hiding comap in lemma induction_aux (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n) (hi : c = (e.1 i).leadingCoeff) (hc : c ≠ 0) : InductionStatement (Away c) n - ⟨C (IsLocalization.Away.invSelf (S := Away c) c) • + ⟨Polynomial.C (IsLocalization.Away.invSelf (S := Away c) c) • mapRingHom (algebraMap _ _) ∘ e.val⟩ → InductionStatement (R ⧸ Ideal.span {c}) n ⟨mapRingHom (algebraMap _ _) ∘ e.val⟩ → InductionStatement R n e := by @@ -193,7 +190,7 @@ lemma induction_aux (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n) set q₂ := Ideal.Quotient.mk (.span {c}) have q₂_surjective : Surjective q₂ := Ideal.Quotient.mk_surjective set e₁ : InductionObj (Away c) n := - ⟨C (IsLocalization.Away.invSelf (S := Away c) c) • mapRingHom q₁ ∘ e.val⟩ + ⟨Polynomial.C (IsLocalization.Away.invSelf (S := Away c) c) • mapRingHom q₁ ∘ e.val⟩ set e₂ : InductionObj (R ⧸ Ideal.span {c}) n := ⟨mapRingHom q₂ ∘ e.val⟩ have degBound_e₁_le : e₁.degBound ≤ e.degBound := by unfold degBound @@ -245,21 +242,21 @@ lemma induction_aux (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n) change (∀ _, q₂ _ = _) at hf₂ -- Lift everything together classical - let S₁ : Finset (Σ n, R × (Fin n → R)) := T₁.image fun x ↦ ⟨_, (c * f₁ x.2.1, g₁ x)⟩ - let S₂ : Finset (Σ n, R × (Fin n → R)) := T₂.image fun x ↦ ⟨_, (f₂ x.2.1, Fin.cons c (g₂ x))⟩ + let S₁ : Finset (R × Σ n, Fin n → R) := T₁.image fun x ↦ ⟨c * f₁ x.1, _, g₁ x⟩ + let S₂ : Finset (R × Σ n, Fin n → R) := T₂.image fun x ↦ ⟨f₂ x.1, _, Fin.cons c (g₂ x)⟩ refine ⟨S₁ ∪ S₂, ?_, ?_⟩ · calc - comap C '' (zeroLocus (.range e.val) \ zeroLocus {f}) - = comap q₁ '' (comap C '' + comap Polynomial.C '' (zeroLocus (.range e.val) \ zeroLocus {f}) + = comap q₁ '' (comap Polynomial.C '' (comap (mapRingHom q₁.toRingHom) ⁻¹' (zeroLocus (.range e.val) \ zeroLocus {f}))) ∪ - comap q₂ '' (comap C '' + comap q₂ '' (comap Polynomial.C '' (comap (mapRingHom q₂) ⁻¹' (zeroLocus (.range e.val) \ zeroLocus {f}))) := Set.image_of_range_union_range_eq_univ (by ext; simp) (by ext; simp) (by rw [← range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, RingHom.algebraMap_toAlgebra]; exact Set.union_compl_self _) _ - _ = (⋃ C ∈ S₁, zeroLocus (Set.range C.snd.2) \ zeroLocus {C.snd.1}) ∪ - ⋃ C ∈ S₂, zeroLocus (Set.range C.snd.2) \ zeroLocus {C.snd.1} := ?_ - _ = ⋃ C ∈ S₁ ∪ S₂, zeroLocus (Set.range C.snd.2) \ zeroLocus {C.snd.1} := by + _ = (⋃ C ∈ S₁, zeroLocus (Set.range C.2.2) \ zeroLocus {C.1}) ∪ + ⋃ C ∈ S₂, zeroLocus (Set.range C.2.2) \ zeroLocus {C.1} := ?_ + _ = ⋃ C ∈ S₁ ∪ S₂, zeroLocus (Set.range C.2.2) \ zeroLocus {C.1} := by simpa using (Set.biUnion_union S₁.toSet S₂ _).symm congr 1 · convert congr(comap q₁.toRingHom '' $hT₁) @@ -282,7 +279,7 @@ lemma induction_aux (R) [CommRing R] (c : R) (i : Fin n) (e : InductionObj R n) swap; · exact localization_specComap_injective _ (.powers c) simp only [AlgHom.toLinearMap_apply] at hq₁g₁ simp only [← Set.range_comp, Function.comp_def, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, - hq₁g₁ _ hxT₁, Set.image_singleton, map_mul, ← hf₁, mul_comm x.2.1, ← mul_assoc, + hq₁g₁ _ hxT₁, Set.image_singleton, map_mul, ← hf₁, mul_comm x.1, ← mul_assoc, ← pow_succ'] simp only [← smul_eq_mul, ← Set.smul_set_range, ← Set.smul_set_singleton, zeroLocus_smul_of_isUnit ((isUnit_of_invertible (q₁ c)).pow _)] @@ -337,7 +334,7 @@ lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus : have : Module.Free R M := .of_basis (AdjoinRoot.powerBasis' hi).basis have : Module.Finite R M := .of_basis (AdjoinRoot.powerBasis' hi).basis refine ⟨(Finset.range (Module.finrank R M)).image - fun j ↦ ⟨0, (Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0⟩, ?_, ?_⟩ + fun j ↦ ⟨(Algebra.lmul R M (Ideal.Quotient.mk _ f)).charpoly.coeff j, 0, 0⟩, ?_, ?_⟩ · ext x have : zeroLocus (Set.range g.val) = zeroLocus {g.1 i} := by rw [Set.range_eq_iUnion, zeroLocus_iUnion] @@ -350,7 +347,7 @@ lemma isConstructible_comap_C_zeroLocus_sdiff_zeroLocus : simp [Set.subset_def, M] · simp · intro R _ f - refine ⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨0, f.coeff j, 0⟩, ?_, ?_⟩ + refine ⟨(Finset.range (f.natDegree + 2)).image fun j ↦ ⟨f.coeff j, 0, 0⟩, ?_, ?_⟩ · convert image_comap_C_basicOpen f · simp only [basicOpen_eq_zeroLocus_compl, Set.compl_eq_univ_diff] congr 1 @@ -456,16 +453,16 @@ lemma exists_constructibleSetData_comap_C_toSet_eq_toSet {R} [CommRing R] (M : Submodule ℤ R) (hM : 1 ∈ M) (S : ConstructibleSetData R[X]) (hS : ∀ x ∈ S, ∀ j k, (x.2.2 j).coeff k ∈ M) : ∃ T : ConstructibleSetData R, - comap C '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.1 ≤ S.degBound ∧ + comap Polynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T, C.2.1 ≤ S.degBound ∧ ∀ i, C.2.2 i ∈ M ^ S.degBound ^ S.degBound := by classical - choose f hf₁ hf₂ hf₃ using fun x : Σ n, R[X] × (Fin n → R[X]) ↦ - isConstructible_comap_C_zeroLocus_sdiff_zeroLocus ⟨x.2.2⟩ x.2.1 + choose f hf₁ hf₂ hf₃ using fun x : R[X] × Σ n, Fin n → R[X] ↦ + isConstructible_comap_C_zeroLocus_sdiff_zeroLocus ⟨x.2.2⟩ x.1 refine ⟨S.biUnion f, ?_, ?_⟩ · simp only [ConstructibleSetData.toSet, Set.image_iUnion, Finset.set_biUnion_biUnion, hf₁] - · simp only [Finset.mem_biUnion, Prod.exists, forall_exists_index, and_imp] + · simp only [Finset.mem_biUnion, forall_exists_index, and_imp] intros x y hy hx - have H : degBound ⟨y.snd.2⟩ ≤ S.degBound := + have H : degBound ⟨y.2.2⟩ ≤ S.degBound := Finset.le_sup (f := fun e ↦ ∑ i, (e.2.2 i).degree.succ) hy refine ⟨(hf₂ y x hx).trans H, fun i ↦ SetLike.le_def.mp ?_ (hf₃ y x hx i)⟩ gcongr @@ -563,43 +560,40 @@ lemma δ_pos (k : ℕ) (D : ℕ → ℕ) : ∀ n, 0 < δ k D n lemma exists_constructibleSetData_comap_C_toSet_eq_toSet' {M : Submodule ℤ R} (hM : 1 ∈ M) (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)) - (hSn : ∀ x ∈ S, x.1 ≤ k) - (hS : ∀ x ∈ S, ∀ j, x.2.2 j ∈ M.mvPolynomial _ ⊓ - (MvPolynomial.degreesLE _ _ d).restrictScalars _) : + (hSn : ∀ x ∈ S, x.2.1 ≤ k) + (hS : ∀ x ∈ S, ∀ j, x.2.2 j ∈ coeffsIn _ M ⊓ (degreesLE _ _ d).restrictScalars _) : ∃ T : ConstructibleSetData R, comap MvPolynomial.C '' S.toSet = T.toSet ∧ ∀ C ∈ T, - C.1 ≤ ν k (fun i ↦ 1 + (d.map Fin.val).count i) n ∧ + C.2.1 ≤ ν k (fun i ↦ 1 + (d.map Fin.val).count i) n ∧ ∀ i, C.2.2 i ∈ M ^ (δ k (fun i ↦ 1 + (d.map Fin.val).count i) n) := by classical induction' n with n IH generalizing k M - · refine ⟨(S.map (MvPolynomial.isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩ + · refine ⟨(S.map (isEmptyRingEquiv _ _).toRingHom), ?_, ?_⟩ · rw [ConstructibleSetData.toSet_map] - show _ = (comapEquiv (MvPolynomial.isEmptyRingEquiv _ _)).symm ⁻¹' _ + show _ = (comapEquiv (isEmptyRingEquiv _ _)).symm ⁻¹' _ rw [← Equiv.image_eq_preimage] rfl - · simp only [Sigma.map, ne_eq, RingEquiv.toRingHom_eq_coe, Finset.mem_image, - Prod.exists, forall_exists_index, and_imp, ConstructibleSetData.map, id_eq, - RingHom.coe_coe, δ_zero, ν_zero, one_mul, pow_one, - MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, - forall_apply_eq_imp_iff₂, comp_apply] + · simp only [Sigma.map, ne_eq, RingEquiv.toRingHom_eq_coe, Finset.mem_image, one_mul, pow_one, + forall_exists_index, and_imp, ConstructibleSetData.map, id_eq, comp_apply, RingHom.coe_coe, + δ_zero, ν_zero, forall_apply_eq_imp_iff₂, isEmptyRingEquiv_eq_coeff_zero] exact fun a haS ↦ ⟨hSn a haS, fun i ↦ (hS a haS i).1 0⟩ let e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] (MvPolynomial (Fin n) R)[X] := - MvPolynomial.finSuccEquiv R n + finSuccEquiv R n let S' := S.map e.toRingHom let hS' : S'.degBound ≤ k * (1 + d.count 0) := by apply Finset.sup_le fun x hxS ↦ ?_ simp only [ConstructibleSetData.map, id_eq, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_coe, Finset.mem_image, Sigma.map, Sigma.exists, Prod.exists, S'] at hxS - obtain ⟨i, f, g, hxS, rfl⟩ := hxS + obtain ⟨f, i, g, hxS, rfl⟩ := hxS trans ∑ i : Fin i, (1 + d.count 0) · gcongr with j hj simp only [e, Function.comp_apply] by_cases hgj : g j = 0 · rw [hgj, map_zero] simp - rw [MvPolynomial.degree_finSuccEquiv hgj, WithBot.succ_natCast, add_comm] - simp only [Nat.cast_id, add_le_add_iff_left, MvPolynomial.degreeOf_def] + rw [degree_finSuccEquiv hgj, WithBot.succ_natCast, add_comm] + simp only [Nat.cast_id, add_le_add_iff_left, degreeOf_def] exact Multiset.count_le_of_le _ (hS _ hxS _).2 · simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul] gcongr @@ -608,39 +602,38 @@ lemma exists_constructibleSetData_comap_C_toSet_eq_toSet' (d.toFinsupp.comapDomain Fin.succ (Fin.succ_injective _).injOn).toMultiset obtain ⟨T, hT₁, hT₂⟩ := exists_constructibleSetData_comap_C_toSet_eq_toSet (R := MvPolynomial (Fin n) R) - (M.mvPolynomial _ ⊓ (MvPolynomial.degreesLE _ _ B).restrictScalars ℤ) + (coeffsIn _ M ⊓ (degreesLE _ _ B).restrictScalars ℤ) (by simpa [MvPolynomial.coeff_one, apply_ite] using hM) S' (fun x hxS j k ↦ by simp only [ConstructibleSetData.map, id_eq, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_coe, Finset.mem_image, Sigma.map, Sigma.exists, Prod.exists, S'] at hxS obtain ⟨i, f, g, hxS, rfl⟩ := hxS - simp only [comp_apply, Submodule.mem_inf, Submodule.mem_mvPolynomial, - Submodule.restrictScalars_mem, MvPolynomial.mem_degreesLE] + simp only [comp_apply, Submodule.mem_inf, mem_coeffsIn, Submodule.restrictScalars_mem, + mem_degreesLE] constructor · intro d - simp only [MvPolynomial.finSuccEquiv_coeff_coeff, e] + simp only [finSuccEquiv_coeff_coeff, e] exact (hS _ hxS _).1 _ - · simp only [MvPolynomial.totalDegree, Finset.sup_le_iff, - MvPolynomial.mem_support_iff, B, - MvPolynomial.finSuccEquiv_coeff_coeff, ne_eq, e] + · simp only [totalDegree, Finset.sup_le_iff, MvPolynomial.mem_support_iff, B, + finSuccEquiv_coeff_coeff, ne_eq, e] replace hS := (hS _ hxS j).2 - simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, MvPolynomial.mem_degreesLE, + simp only [Submodule.coe_restrictScalars, SetLike.mem_coe, mem_degreesLE, Multiset.le_iff_count, Finsupp.count_toMultiset, Finsupp.comapDomain_apply, - Multiset.toFinsupp_apply, ← MvPolynomial.degreeOf_def] at hS ⊢ + Multiset.toFinsupp_apply, ← degreeOf_def] at hS ⊢ intro a - exact (MvPolynomial.degreeOf_coeff_finSuccEquiv (g j) a k).trans (hS _)) + exact (degreeOf_coeff_finSuccEquiv (g j) a k).trans (hS _)) have (C hCT k) := SetLike.le_def.mp pow_inf_le ((hT₂ C hCT).2 k) - replace this (C hCT k) := SetLike.le_def.mp (inf_le_inf_right _ Submodule.mvPolynomial_pow_le) + replace this (C hCT k) := SetLike.le_def.mp (inf_le_inf_right _ le_coeffsIn_pow) (this C hCT k) let N := (k * (1 + d.count 0)) ^ (k * (1 + d.count 0)) - have (C) (hCT : C ∈ T) (a) : C.snd.2 a ∈ (M ^ N).mvPolynomial (Fin n) ⊓ - (MvPolynomial.degreesLE R (Fin n) (N • B)).restrictScalars ℤ := by + have (C) (hCT : C ∈ T) (a) : C.2.2 a ∈ coeffsIn (Fin n) (M ^ N) ⊓ + (degreesLE R (Fin n) (N • B)).restrictScalars ℤ := by refine SetLike.le_def.mp ?_ ((hT₂ C hCT).2 a) refine pow_inf_le.trans (inf_le_inf ?_ ?_) - · refine (pow_le_pow_right' ?_ (Nat.pow_self_mono hS')).trans Submodule.mvPolynomial_pow_le + · refine (pow_le_pow_right' ?_ (Nat.pow_self_mono hS')).trans le_coeffsIn_pow simpa [MvPolynomial.coeff_one, apply_ite] using hM - · rw [← MvPolynomial.degreesLE_pow, Submodule.restrictScalars_pow Nat.pow_self_pos.ne'] + · rw [← degreesLE_pow, Submodule.restrictScalars_pow Nat.pow_self_pos.ne'] refine pow_le_pow_right' ?_ (Nat.pow_self_mono hS') simp have h1M : 1 ≤ M := Submodule.one_le.mpr hM @@ -677,30 +670,29 @@ lemma exists_constructibleSetData_comap_C_toSet_eq_toSet' ((δ_casesOn_succ k _ _ _).symm.trans_le (δ_le_δ le_rfl _ this)) simp +contextual [mul_add, Nat.one_le_iff_ne_zero] -lemma chevalley_mvPolynomial_mvPolynomial +lemma chevalley_coeffsIn_coeffsIn {n m : ℕ} (f : MvPolynomial (Fin m) R →ₐ[R] MvPolynomial (Fin n) R) (k : ℕ) (d : Multiset (Fin n)) (S : ConstructibleSetData (MvPolynomial (Fin n) R)) - (hSn : ∀ x ∈ S, x.1 ≤ k) + (hSn : ∀ x ∈ S, x.2.1 ≤ k) (hS : ∀ x ∈ S, ∀ j, (x.2.2 j).degrees ≤ d) (hf : ∀ i, (f (.X i)).degrees ≤ d) : ∃ T : ConstructibleSetData (MvPolynomial (Fin m) R), comap f '' S.toSet = T.toSet ∧ - ∀ C ∈ T, C.1 ≤ ν (k + m) (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧ - ∀ i j, MvPolynomial.degreeOf j (C.2.2 i) ≤ - δ (k + m) (fun i ↦ 1 + (d.map Fin.val).count i) n := by + ∀ C ∈ T, C.2.1 ≤ ν (k + m) (fun i ↦ 1 + Multiset.count i (Multiset.map Fin.val d)) n ∧ + ∀ i j, (C.2.2 i).degreeOf j ≤ δ (k + m) (fun i ↦ 1 + (d.map Fin.val).count i) n := by classical let g : MvPolynomial (Fin n) (MvPolynomial (Fin m) R) →+* MvPolynomial (Fin n) R := - MvPolynomial.eval₂Hom f.toRingHom MvPolynomial.X + eval₂Hom f.toRingHom X have hg : g.comp (algebraMap (MvPolynomial (Fin m) R) _) = f := by ext x : 2 <;> simp [g] let σ : MvPolynomial (Fin n) R →+* MvPolynomial (Fin n) (MvPolynomial (Fin m) R) := - MvPolynomial.map (algebraMap _ _) + map (algebraMap _ _) have hσ : g.comp σ = .id _ := by ext : 2 <;> simp [g, σ] have hσ' (x) : g (σ x) = x := DFunLike.congr_fun hσ x have hg' : Function.Surjective g := LeftInverse.surjective hσ' let S' : ConstructibleSetData (MvPolynomial (Fin n) (MvPolynomial (Fin m) R)) := S.image - fun ⟨k, fk, gk⟩ ↦ ⟨k + m, σ fk, fun s ↦ (finSumFinEquiv.symm s).elim (σ ∘ gk) + fun ⟨fk, k, gk⟩ ↦ ⟨σ fk, k + m, fun s ↦ (finSumFinEquiv.symm s).elim (σ ∘ gk) fun i ↦ .C (.X i) - σ (f (.X i))⟩ let s₀ : Set (MvPolynomial (Fin n) (MvPolynomial (Fin m) R)) := Set.range fun i ↦ .C (.X i) - σ (f (.X i)) @@ -714,21 +706,21 @@ lemma chevalley_mvPolynomial_mvPolynomial refine H.antisymm fun p hp ↦ ?_ obtain ⟨q₁, q₂, hq₁, rfl⟩ : ∃ q₁ q₂, q₁ ∈ Ideal.span s₀ ∧ p = q₁ + σ q₂ := by clear hp - obtain ⟨p, rfl⟩ := (MvPolynomial.commAlgEquiv _ _ _).surjective p - simp_rw [← (MvPolynomial.commAlgEquiv R (Fin m) (Fin n)).symm.injective.eq_iff, + obtain ⟨p, rfl⟩ := (commAlgEquiv _ _ _).surjective p + simp_rw [← (commAlgEquiv R (Fin m) (Fin n)).symm.injective.eq_iff, AlgEquiv.symm_apply_apply] induction p using MvPolynomial.induction_on with | h_C q => - exact ⟨0, q, by simp, (MvPolynomial.commAlgEquiv _ _ _).injective <| - by simp [MvPolynomial.commAlgEquiv_C, σ]⟩ + exact ⟨0, q, by simp, (commAlgEquiv _ _ _).injective <| + by simp [commAlgEquiv_C, σ]⟩ | h_add p q hp hq => obtain ⟨q₁, q₂, hq₁, rfl⟩ := hp obtain ⟨q₃, q₄, hq₃, rfl⟩ := hq refine ⟨q₁ + q₃, q₂ + q₄, add_mem hq₁ hq₃, by simp only [map_add, add_add_add_comm]⟩ | h_X p i hp => obtain ⟨q₁, q₂, hq₁, rfl⟩ := hp - simp only [← (MvPolynomial.commAlgEquiv R (Fin m) (Fin n)).injective.eq_iff, - map_mul, AlgEquiv.apply_symm_apply, MvPolynomial.commAlgEquiv_X] + simp only [← (commAlgEquiv R (Fin m) (Fin n)).injective.eq_iff, + map_mul, AlgEquiv.apply_symm_apply, commAlgEquiv_X] refine ⟨q₁ * .C (.X i) + σ q₂ * (.C (.X i) - σ (f (.X i))), q₂ * f (.X i), ?_, ?_⟩ · exact add_mem (Ideal.mul_mem_right _ _ hq₁) (Ideal.mul_mem_left _ _ (Ideal.subset_span (Set.mem_range_self _))) @@ -751,38 +743,37 @@ lemma chevalley_mvPolynomial_mvPolynomial simp [hg'', ← Set.inter_diff_distrib_right, Set.sdiff_inter_right_comm, s₀] obtain ⟨T, hT, hT'⟩ := exists_constructibleSetData_comap_C_toSet_eq_toSet' - (M := (MvPolynomial.degreesLE R (Fin m) Finset.univ.1).restrictScalars ℤ) (by simp) (k + m) d S' + (M := (degreesLE R (Fin m) Finset.univ.1).restrictScalars ℤ) (by simp) (k + m) d S' (Finset.forall_mem_image.mpr fun x hx ↦ (by simpa using hSn _ hx)) (Finset.forall_mem_image.mpr fun x hx ↦ by intro j obtain ⟨j, rfl⟩ := finSumFinEquiv.surjective j - simp only [Equiv.symm_apply_apply, Submodule.mem_inf, Submodule.mem_mvPolynomial, - implies_true, Submodule.restrictScalars_mem, MvPolynomial.mem_degreesLE, - true_and] + simp only [Equiv.symm_apply_apply, Submodule.mem_inf, mem_coeffsIn, implies_true, + Submodule.restrictScalars_mem, mem_degreesLE, true_and] constructor · intro i cases' j with j j - · simp [σ, MvPolynomial.coeff_map, MvPolynomial.degrees_C] - · simp only [MvPolynomial.algebraMap_eq, Sum.elim_inr, MvPolynomial.coeff_sub, - MvPolynomial.coeff_C, MvPolynomial.coeff_map, σ] - refine (MvPolynomial.degrees_sub _ _).trans ?_ - simp only [MvPolynomial.degrees_C, apply_ite, MvPolynomial.degrees_zero] - simp only [zero_le, sup_of_le_left] + · simp [σ, MvPolynomial.coeff_map, degrees_C] + · simp only [algebraMap_eq, Sum.elim_inr, coeff_sub, MvPolynomial.coeff_C, + MvPolynomial.coeff_map, σ] + refine degrees_sub_le.trans ?_ + simp only [degrees_C, apply_ite, degrees_zero, + Multiset.union_zero] split_ifs with h - · refine (MvPolynomial.degrees_X' _).trans ?_ + · refine (degrees_X' _).trans ?_ simp · simp · cases' j with j j - · simp only [MvPolynomial.algebraMap_eq, Sum.elim_inl, comp_apply, σ] - exact (MvPolynomial.degrees_map_le _ _).trans (hS _ hx j) - · refine (MvPolynomial.degrees_sub _ _).trans ?_ - simp only [MvPolynomial.degrees_C, zero_le, sup_of_le_right] - exact (MvPolynomial.degrees_map_le _ _).trans (hf _)) + · simp only [algebraMap_eq, Sum.elim_inl, comp_apply, σ] + exact degrees_map_le.trans (hS _ hx j) + · refine degrees_sub_le.trans ?_ + simp only [degrees_C, Multiset.zero_union] + exact degrees_map_le.trans (hf _)) refine ⟨T, ?_, fun C hCT ↦ ⟨(hT' C hCT).1, fun i j ↦ ?_⟩⟩ · rwa [← hg, comap_comp, ContinuousMap.coe_comp, Set.image_comp, hS'] · have := (hT' C hCT).2 i - rw [← Submodule.restrictScalars_pow (δ_pos ..).ne', MvPolynomial.degreesLE_pow, - Submodule.restrictScalars_mem, MvPolynomial.mem_degreesLE, + rw [← Submodule.restrictScalars_pow (δ_pos ..).ne', degreesLE_pow, + Submodule.restrictScalars_mem, mem_degreesLE, Multiset.le_iff_count] at this - simpa only [Multiset.count_nsmul, Multiset.count_univ, mul_one, ← MvPolynomial.degreeOf_def] + simpa only [Multiset.count_nsmul, Multiset.count_univ, mul_one, ← degreeOf_def] using this j diff --git a/LeanCamCombi/GrowthInGroups/Constructible.lean b/LeanCamCombi/GrowthInGroups/Constructible.lean deleted file mode 100644 index c4b4472c53..0000000000 --- a/LeanCamCombi/GrowthInGroups/Constructible.lean +++ /dev/null @@ -1,425 +0,0 @@ -/- -Copyright (c) 2024 Yaël Dillies. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yaël Dillies --/ -import Mathlib.Order.BooleanSubalgebra -import Mathlib.Topology.Spectral.Hom - -/-! -# Constructible sets - -This file defines constructible sets, which are morally sets in a topological space which we can -make out of finite unions and intersections of open and closed sets. - -Precisely, constructible sets are the boolean subalgebra generated by open retrocompact sets, -where a set is retrocompact if its intersection with every compact open set is compact. - -Constructible sets are useful because the image of a constructible set under a finitely presented -morphism of schemes is a constructible set (and this is *not* true at the level of varieties). - -## Main declarations - -* `IsRetrocompact`: Predicate for a set to be retrocompact, namely to have its intersection with - every compact open is compact. -* `IsConstructible`: Predicate for a set to be constructible, namely to belong to the boolean - subalgebra generated by open retrocompact sets. -* `IsLocallyConstructible`: Predicate for a set to be locally constructible, namely to be - partitionable along an open cover such that each of its parts is constructible. --/ - -open Set TopologicalSpace Topology -open scoped Set.Notation - -variable {ι : Sort*} {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} - {s t U : Set X} {a : X} - -/-! ### retrocompact sets -/ - -/-- A retrocompact set is a set whose intersection with every compact open is compact. -/ -@[stacks 005A] -def IsRetrocompact (s : Set X) : Prop := ∀ ⦃U⦄, IsCompact U → IsOpen U → IsCompact (s ∩ U) - -@[simp] lemma IsRetrocompact.empty : IsRetrocompact (∅ : Set X) := by simp [IsRetrocompact] -@[simp] lemma IsRetrocompact.univ : IsRetrocompact (univ : Set X) := by - simp +contextual [IsRetrocompact] - -@[simp] lemma IsRetrocompact.singleton : IsRetrocompact {a} := - fun _ _ _ ↦ Subsingleton.singleton_inter.isCompact - -lemma IsRetrocompact.union (hs : IsRetrocompact s) (ht : IsRetrocompact t) : - IsRetrocompact (s ∪ t : Set X) := - fun _U hUcomp hUopen ↦ union_inter_distrib_right .. ▸ (hs hUcomp hUopen).union (ht hUcomp hUopen) - -private lemma supClosed_isRetrocompact : SupClosed {s : Set X | IsRetrocompact s} := - fun _s hs _t ht ↦ hs.union ht - -lemma IsRetrocompact.finsetSup {ι : Type*} {s : Finset ι} {t : ι → Set X} - (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.sup t) := by - induction' s using Finset.cons_induction with i s ih hi - · simp - · rw [Finset.sup_cons] - exact (ht _ <| by simp).union <| hi <| Finset.forall_of_forall_cons ht - -set_option linter.docPrime false in -lemma IsRetrocompact.finsetSup' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X} - (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.sup' hs t) := by - rw [Finset.sup'_eq_sup]; exact .finsetSup ht - -lemma IsRetrocompact.iUnion [Finite ι] {f : ι → Set X} (hf : ∀ i, IsRetrocompact (f i)) : - IsRetrocompact (⋃ i, f i) := supClosed_isRetrocompact.iSup_mem .empty hf - -lemma IsRetrocompact.sUnion {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsRetrocompact s) : - IsRetrocompact (⋃₀ S) := supClosed_isRetrocompact.sSup_mem hS .empty hS' - -lemma IsRetrocompact.biUnion {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite) - (hf : ∀ i ∈ t, IsRetrocompact (f i)) : IsRetrocompact (⋃ i ∈ t, f i) := - supClosed_isRetrocompact.biSup_mem ht .empty hf - -section T2Space -variable [T2Space X] - -lemma IsRetrocompact.inter (hs : IsRetrocompact s) (ht : IsRetrocompact t) : - IsRetrocompact (s ∩ t : Set X) := - fun _U hUcomp hUopen ↦ inter_inter_distrib_right .. ▸ (hs hUcomp hUopen).inter (ht hUcomp hUopen) - -private lemma infClosed_isRetrocompact : InfClosed {s : Set X | IsRetrocompact s} := - fun _s hs _t ht ↦ hs.inter ht - -lemma IsRetrocompact.finsetInf {ι : Type*} {s : Finset ι} {t : ι → Set X} - (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.inf t) := by - induction' s using Finset.cons_induction with i s ih hi - · simp - · rw [Finset.inf_cons] - exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht - -set_option linter.docPrime false in -lemma IsRetrocompact.finsetInf' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X} - (ht : ∀ i ∈ s, IsRetrocompact (t i)) : IsRetrocompact (s.inf' hs t) := by - rw [Finset.inf'_eq_inf]; exact .finsetInf ht - -lemma IsRetrocompact.iInter [Finite ι] {f : ι → Set X} (hf : ∀ i, IsRetrocompact (f i)) : - IsRetrocompact (⋂ i, f i) := infClosed_isRetrocompact.iInf_mem .univ hf - -lemma IsRetrocompact.sInter {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsRetrocompact s) : - IsRetrocompact (⋂₀ S) := infClosed_isRetrocompact.sInf_mem hS .univ hS' - -lemma IsRetrocompact.biInter {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite) - (hf : ∀ i ∈ t, IsRetrocompact (f i)) : IsRetrocompact (⋂ i ∈ t, f i) := - infClosed_isRetrocompact.biInf_mem ht .univ hf - -end T2Space - -lemma IsRetrocompact.inter_isOpen (hs : IsRetrocompact s) (ht : IsRetrocompact t) - (htopen : IsOpen t) : IsRetrocompact (s ∩ t : Set X) := - fun _U hUcomp hUopen ↦ inter_assoc .. ▸ hs (ht hUcomp hUopen) (htopen.inter hUopen) - -lemma IsRetrocompact.isOpen_inter (hs : IsRetrocompact s) (ht : IsRetrocompact t) - (hsopen : IsOpen s) : IsRetrocompact (s ∩ t : Set X) := - inter_comm .. ▸ ht.inter_isOpen hs hsopen - -lemma IsRetrocompact_iff_isSpectralMap_subtypeVal : - IsRetrocompact s ↔ IsSpectralMap (Subtype.val : s → X) := by - refine ⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩ - · rw [IsEmbedding.subtypeVal.isCompact_iff, image_preimage_eq_inter_range, - Subtype.range_coe_subtype, setOf_mem_eq, inter_comm] - exact hs htcomp htopen - · simpa using (hs.isCompact_preimage_of_isOpen htopen htcomp).image continuous_subtype_val - -@[stacks 005B] -lemma IsRetrocompact.image_of_isEmbedding (hs : IsRetrocompact s) (hfemb : IsEmbedding f) - (hfcomp : IsRetrocompact (range f)) : IsRetrocompact (f '' s) := by - rintro U hUcomp hUopen - rw [← image_inter_preimage, ← hfemb.isCompact_iff] - refine hs ?_ <| hUopen.preimage hfemb.continuous - rw [hfemb.isCompact_iff, image_preimage_eq_inter_range, inter_comm] - exact hfcomp hUcomp hUopen - -@[stacks 005J] -- Extracted from the proof of `005J` -lemma IsRetrocompact.preimage_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f) - (hs : IsRetrocompact s) : IsRetrocompact (f ⁻¹' s) := by - rintro U hUcomp hUopen - rw [hf.isCompact_iff, image_preimage_inter] - exact hs (hUcomp.image hf.continuous) <| hf.isOpenMap _ hUopen - -@[stacks 09YE] -- Extracted from the proof of `09YE` -lemma IsRetrocompact.preimage_of_isClosedEmbedding {s : Set Y} (hf : IsClosedEmbedding f) - (hf' : IsCompact (range f)ᶜ) (hs : IsRetrocompact s) : IsRetrocompact (f ⁻¹' s) := by - rintro U hUcomp hUopen - have hfUopen : IsOpen (f '' U ∪ (range f)ᶜ) := by - simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm] - using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl - have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf' - simpa [inter_union_distrib_left, inter_left_comm, inter_eq_right.2 (image_subset_range ..), - hf.isCompact_iff, image_preimage_inter] using (hs hfUcomp hfUopen).inter_left hf.isClosed_range - -/-! ### Constructible sets -/ - -namespace Topology - -/-- A constructible set is a set that can be written as the -finite union/finite intersection/complement of open retrocompact sets. - -In other words, constructible sets form the boolean subalgebra generated by open retrocompact sets. --/ -def IsConstructible (s : Set X) : Prop := - s ∈ BooleanSubalgebra.closure {U | IsOpen U ∧ IsRetrocompact U} - -@[simp] -protected lemma IsConstructible.empty : IsConstructible (∅ : Set X) := BooleanSubalgebra.bot_mem - -@[simp] -protected lemma IsConstructible.univ : IsConstructible (univ : Set X) := BooleanSubalgebra.top_mem - -lemma IsConstructible.union : IsConstructible s → IsConstructible t → IsConstructible (s ∪ t) := - BooleanSubalgebra.sup_mem - -lemma IsConstructible.inter : IsConstructible s → IsConstructible t → IsConstructible (s ∩ t) := - BooleanSubalgebra.inf_mem - -lemma IsConstructible.sdiff : IsConstructible s → IsConstructible t → IsConstructible (s \ t) := - BooleanSubalgebra.sdiff_mem - -lemma IsConstructible.himp : IsConstructible s → IsConstructible t → IsConstructible (s ⇨ t) := - BooleanSubalgebra.himp_mem - -@[simp] lemma isConstructible_compl : IsConstructible sᶜ ↔ IsConstructible s := - BooleanSubalgebra.compl_mem_iff - -alias ⟨IsConstructible.of_compl, IsConstructible.compl⟩ := isConstructible_compl - -lemma IsConstructible.iUnion [Finite ι] {f : ι → Set X} (hf : ∀ i, IsConstructible (f i)) : - IsConstructible (⋃ i, f i) := BooleanSubalgebra.iSup_mem hf - -lemma IsConstructible.iInter [Finite ι] {f : ι → Set X} (hf : ∀ i, IsConstructible (f i)) : - IsConstructible (⋂ i, f i) := BooleanSubalgebra.iInf_mem hf - -lemma IsConstructible.sUnion {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsConstructible s) : - IsConstructible (⋃₀ S) := BooleanSubalgebra.sSup_mem hS hS' - -lemma IsConstructible.sInter {S : Set (Set X)} (hS : S.Finite) (hS' : ∀ s ∈ S, IsConstructible s) : - IsConstructible (⋂₀ S) := BooleanSubalgebra.sInf_mem hS hS' - -lemma IsConstructible.biUnion {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite) - (hf : ∀ i ∈ t, IsConstructible (f i)) : IsConstructible (⋃ i ∈ t, f i) := - BooleanSubalgebra.biSup_mem ht hf - -lemma IsConstructible.biInter {ι : Type*} {f : ι → Set X} {t : Set ι} (ht : t.Finite) - (hf : ∀ i ∈ t, IsConstructible (f i)) : IsConstructible (⋂ i ∈ t, f i) := - BooleanSubalgebra.biInf_mem ht hf - -lemma _root_.IsRetrocompact.isConstructible (hUopen : IsOpen U) (hUcomp : IsRetrocompact U) : - IsConstructible U := BooleanSubalgebra.subset_closure ⟨hUopen, hUcomp⟩ - -/-- An induction principle for constructible sets. If `p` holds for all open retrocompact -sets, and is preserved under union and complement, then `p` holds for all constructible sets. -/ -@[elab_as_elim] -lemma IsConstructible.empty_union_induction {p : ∀ s : Set X, IsConstructible s → Prop} - (open_retrocompact : ∀ U (hUopen : IsOpen U) (hUcomp : IsRetrocompact U), - p U (BooleanSubalgebra.subset_closure ⟨hUopen, hUcomp⟩)) - (union : ∀ s hs t ht, p s hs → p t ht → p (s ∪ t) (hs.union ht)) - (compl : ∀ s hs, p s hs → p sᶜ hs.compl) {s} (hs : IsConstructible s) : p s hs := by - induction hs using BooleanSubalgebra.closure_bot_sup_induction with - | mem U hU => exact open_retrocompact _ hU.1 hU.2 - | bot => exact open_retrocompact _ isOpen_empty .empty - | sup s hs t ht hs' ht' => exact union _ _ _ _ hs' ht' - | compl s hs hs' => exact compl _ _ hs' - -/-- If `f` is continuous and is such that preimages of retrocompact sets are retrocompact, then -preimages of constructible sets are constructible. -/ -@[stacks 005I] -lemma IsConstructible.preimage {s : Set Y} (hfcont : Continuous f) - (hf : ∀ s, IsRetrocompact s → IsRetrocompact (f ⁻¹' s)) (hs : IsConstructible s) : - IsConstructible (f ⁻¹' s) := by - induction hs using IsConstructible.empty_union_induction with - | open_retrocompact U hUopen hUcomp => - exact (hf _ hUcomp).isConstructible <| hUopen.preimage hfcont - | union s hs t ht hs' ht' => rw [preimage_union]; exact hs'.union ht' - | compl s hs hs' => rw [preimage_compl]; exact hs'.compl - -@[stacks 005J] -lemma IsConstructible.preimage_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f) - (hs : IsConstructible s) : IsConstructible (f ⁻¹' s) := - hs.preimage hf.continuous fun _t ht ↦ ht.preimage_of_isOpenEmbedding hf - -@[stacks 09YE] -lemma IsConstructible.preimage_of_isClosedEmbedding {s : Set Y} (hf : IsClosedEmbedding f) - (hf' : IsCompact (range f)ᶜ) (hs : IsConstructible s) : IsConstructible (f ⁻¹' s) := - hs.preimage hf.continuous fun _t ht ↦ ht.preimage_of_isClosedEmbedding hf hf' - -@[stacks 09YD] -lemma IsConstructible.image_of_isOpenEmbedding (hfopen : IsOpenEmbedding f) - (hfcomp : IsRetrocompact (range f)) (hs : IsConstructible s) : IsConstructible (f '' s) := by - induction hs using IsConstructible.empty_union_induction with - | open_retrocompact U hUopen hUcomp => - exact (hUcomp.image_of_isEmbedding hfopen.isEmbedding hfcomp).isConstructible <| - hfopen.isOpenMap _ hUopen - | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht' - | compl s hs hs' => - rw [← range_diff_image hfopen.injective] - exact (hfcomp.isConstructible hfopen.isOpen_range).sdiff hs' - -@[stacks 09YG] -lemma IsConstructible.image_of_isClosedEmbedding (hf : IsClosedEmbedding f) - (hfcomp : IsRetrocompact (range f)ᶜ) (hs : IsConstructible s) : IsConstructible (f '' s) := by - induction hs using IsConstructible.empty_union_induction with - | open_retrocompact U hUopen hUcomp => - have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by - simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm] - using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl - suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by - simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)] - using (h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl) - rintro V hVcomp hVopen - rw [union_inter_distrib_right, ← image_inter_preimage] - exact ((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image - hf.continuous).union <| hfcomp hVcomp hVopen - | union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht' - | compl s hs hs' => - rw [← range_diff_image hf.injective] - exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs' - -lemma isConstructible_preimage_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f) - (hfcomp : IsRetrocompact (range f)) (hsf : s ⊆ range f) : - IsConstructible (f ⁻¹' s) ↔ IsConstructible s where - mp hs := by simpa [image_preimage_eq_range_inter, inter_eq_right.2 hsf] - using hs.image_of_isOpenEmbedding hf hfcomp - mpr := .preimage_of_isOpenEmbedding hf - -section CompactSpace -variable [CompactSpace X] {P : ∀ s : Set X, IsConstructible s → Prop} {B : Set (Set X)} - {b : ι → Set X} - -lemma _root_.IsRetrocompact.isCompact (hs : IsRetrocompact s) : IsCompact s := by - simpa using hs CompactSpace.isCompact_univ - -lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact - (basis : IsTopologicalBasis B) (compact_inter : ∀ U ∈ B, ∀ V ∈ B, IsCompact (U ∩ V)) - (hU : IsOpen U) : IsRetrocompact U ↔ IsCompact U := by - refine ⟨IsRetrocompact.isCompact, fun hU' {V} hV' hV ↦ ?_⟩ - obtain ⟨s, rfl⟩ := eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _ basis _ hU' hU - obtain ⟨t, rfl⟩ := eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open _ basis _ hV' hV - rw [Set.sUnion_inter_sUnion] - refine ((s.finite_toSet.image _).prod (t.finite_toSet.image _)).isCompact_biUnion ?_ - simp only [mem_prod, mem_image, Finset.mem_coe, Subtype.exists, exists_and_right, exists_eq_right, - and_imp, forall_exists_index, Prod.forall] - exact fun u v hu _ hv _ ↦ compact_inter _ hu _ hv - -lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact_iff_isCompact' - (basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j)) - (hU : IsOpen U) : IsRetrocompact U ↔ IsCompact U := - basis.isRetrocompact_iff_isCompact (by simpa using compact_inter) hU - -lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact (basis : IsTopologicalBasis B) - (compact_inter : ∀ U ∈ B, ∀ V ∈ B, IsCompact (U ∩ V)) (hU : U ∈ B) : IsRetrocompact U := - (basis.isRetrocompact_iff_isCompact compact_inter <| basis.isOpen hU).2 <| by - simpa using compact_inter _ hU _ hU - -/-- Variant of `TopologicalSpace.IsTopologicalBasis.isRetrocompact` for an indexed topological -basis. -/ -lemma _root_.TopologicalSpace.IsTopologicalBasis.isRetrocompact' - (basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j)) (i : ι) : - IsRetrocompact (b i) := - (basis.isRetrocompact_iff_isCompact' compact_inter <| basis.isOpen <| mem_range_self _).2 <| by - simpa using compact_inter i i - -lemma _root_.TopologicalSpace.IsTopologicalBasis.isConstructible (basis : IsTopologicalBasis B) - (compact_inter : ∀ U ∈ B, ∀ V ∈ B, IsCompact (U ∩ V)) (hU : U ∈ B) : IsConstructible U := - (basis.isRetrocompact compact_inter hU).isConstructible <| basis.isOpen hU - -/-- Variant of `TopologicalSpace.IsTopologicalBasis.isConstructible` for an indexed topological -basis. -/ -lemma _root_.TopologicalSpace.IsTopologicalBasis.isConstructible' - (basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j)) (i : ι) : - IsConstructible (b i) := - (basis.isRetrocompact' compact_inter _).isConstructible <| basis.isOpen <| mem_range_self _ - -@[elab_as_elim] -lemma IsConstructible.induction_of_isTopologicalBasis {ι : Type*} [Nonempty ι] (b : ι → Set X) - (basis : IsTopologicalBasis (range b)) (compact_inter : ∀ i j, IsCompact (b i ∩ b j)) - (sdiff : ∀ i s (hs : Set.Finite s), P (b i \ ⋃ j ∈ s, b j) - ((basis.isConstructible' compact_inter _).sdiff <| .biUnion hs fun _ _ ↦ - basis.isConstructible' compact_inter _)) - (union : ∀ s hs t ht, P s hs → P t ht → P (s ∪ t) (hs.union ht)) - (s : Set X) (hs : IsConstructible s) : P s hs := by - induction s, hs using BooleanSubalgebra.closure_sdiff_sup_induction with - | isSublattice => - exact ⟨fun s hs t ht ↦ ⟨hs.1.union ht.1, hs.2.union ht.2⟩, - fun s hs t ht ↦ ⟨hs.1.inter ht.1, hs.2.inter_isOpen ht.2 ht.1⟩⟩ - | bot_mem => exact ⟨isOpen_empty, .empty⟩ - | top_mem => exact ⟨isOpen_univ, .univ⟩ - | sdiff U hU V hV => - have := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _ basis - fun i ↦ by simpa using compact_inter i i - obtain ⟨s, hs, rfl⟩ := (this _).1 ⟨hU.2.isCompact, hU.1⟩ - obtain ⟨t, ht, rfl⟩ := (this _).1 ⟨hV.2.isCompact, hV.1⟩ - simp_rw [iUnion_diff] - induction s, hs using Set.Finite.induction_on with - | empty => simpa using sdiff (Classical.arbitrary _) {Classical.arbitrary _} - | @insert i s hi hs ih => - simp_rw [biUnion_insert] - exact union _ _ _ - (.biUnion hs fun i _ ↦ (basis.isConstructible' compact_inter _).sdiff <| - .biUnion ht fun j _ ↦ basis.isConstructible' compact_inter _) - (sdiff _ _ ht) - (ih ⟨isOpen_biUnion fun _ _ ↦ basis.isOpen ⟨_, rfl⟩, .biUnion hs - fun i _ ↦ basis.isRetrocompact' compact_inter _⟩) - | sup s _ t _ hs' ht' => exact union _ _ _ _ hs' ht' - -end CompactSpace - -/-! ### Locally constructible sets -/ - -/-- A set in a topological space is locally constructible, if every point has a neighborhood on -which the set is constructible. -/ -@[stacks 005G] -def IsLocallyConstructible (s : Set X) : Prop := ∀ x, ∃ U ∈ 𝓝 x, IsOpen U ∧ IsConstructible (U ↓∩ s) - -lemma IsConstructible.isLocallyConstructible (hs : IsConstructible s) : IsLocallyConstructible s := - fun _ ↦ ⟨univ, by simp, by simp, - (isConstructible_preimage_of_isOpenEmbedding isOpen_univ.isOpenEmbedding_subtypeVal (by simp) - (by simp)).2 hs⟩ - -lemma _root_.IsRetrocompact.isLocallyConstructible (hUopen : IsOpen U) (hUcomp : IsRetrocompact U) : - IsLocallyConstructible U := (hUcomp.isConstructible hUopen).isLocallyConstructible - -@[simp] protected lemma IsLocallyConstructible.empty : IsLocallyConstructible (∅ : Set X) := - IsConstructible.empty.isLocallyConstructible - -@[simp] protected lemma IsLocallyConstructible.univ : IsLocallyConstructible (univ : Set X) := - IsConstructible.univ.isLocallyConstructible - -lemma IsLocallyConstructible.inter (hs : IsLocallyConstructible s) (ht : IsLocallyConstructible t) : - IsLocallyConstructible (s ∩ t) := by - rintro x - obtain ⟨U, hxU, hU, hsU⟩ := hs x - obtain ⟨V, hxV, hV, htV⟩ := ht x - refine ⟨U ∩ V, Filter.inter_mem hxU hxV, hU.inter hV, ?_⟩ - change IsConstructible - (inclusion inter_subset_left ⁻¹' (U ↓∩ s) ∩ inclusion inter_subset_right ⁻¹' (V ↓∩ t)) - sorry - -lemma IsLocallyConstructible.finsetInf {ι : Type*} {s : Finset ι} {t : ι → Set X} - (ht : ∀ i ∈ s, IsLocallyConstructible (t i)) : IsLocallyConstructible (s.inf t) := by - induction' s using Finset.cons_induction with i s ih hi - · simp - · rw [Finset.inf_cons] - exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht - -set_option linter.docPrime false in -lemma IsLocallyConstructible.finsetInf' {ι : Type*} {s : Finset ι} {hs} {t : ι → Set X} - (ht : ∀ i ∈ s, IsLocallyConstructible (t i)) : IsLocallyConstructible (s.inf' hs t) := by - rw [Finset.inf'_eq_inf]; exact .finsetInf ht - -private lemma infClosed_isLocallyConstructible : InfClosed {s : Set X | IsLocallyConstructible s} := - fun _s hs _t ht ↦ hs.inter ht - -lemma IsLocallyConstructible.iInter [Finite ι] {f : ι → Set X} - (hf : ∀ i, IsLocallyConstructible (f i)) : IsLocallyConstructible (⋂ i, f i) := - infClosed_isLocallyConstructible.iInf_mem .univ hf - -lemma IsLocallyConstructible.sInter {S : Set (Set X)} (hS : S.Finite) - (hS' : ∀ s ∈ S, IsLocallyConstructible s) : IsLocallyConstructible (⋂₀ S) := - infClosed_isLocallyConstructible.sInf_mem hS .univ hS' - -end Topology diff --git a/LeanCamCombi/GrowthInGroups/ConstructiblePrimeSpectrum.lean b/LeanCamCombi/GrowthInGroups/ConstructiblePrimeSpectrum.lean deleted file mode 100644 index 913d16f197..0000000000 --- a/LeanCamCombi/GrowthInGroups/ConstructiblePrimeSpectrum.lean +++ /dev/null @@ -1,13 +0,0 @@ -import Mathlib.RingTheory.Spectrum.Prime.Topology -import LeanCamCombi.GrowthInGroups.Constructible - -namespace PrimeSpectrum -variable {R : Type*} [CommSemiring R] - -lemma isRetrocompact_iff {U : Set (PrimeSpectrum R)} (hU : IsOpen U) : - IsRetrocompact U ↔ IsCompact U := by - refine isTopologicalBasis_basic_opens.isRetrocompact_iff_isCompact ?_ hU - simpa [← TopologicalSpace.Opens.coe_inf, ← basicOpen_mul, -basicOpen_eq_zeroLocus_compl] - using fun _ _ ↦ isCompact_basicOpen _ - -end PrimeSpectrum diff --git a/LeanCamCombi/GrowthInGroups/ConstructibleSetData.lean b/LeanCamCombi/GrowthInGroups/ConstructibleSetData.lean deleted file mode 100644 index 806b9a873a..0000000000 --- a/LeanCamCombi/GrowthInGroups/ConstructibleSetData.lean +++ /dev/null @@ -1,63 +0,0 @@ -/- -Copyright (c) 2024 Yaël Dillies, Andrew Yang. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yaël Dillies, Andrew Yang --/ -import Mathlib.RingTheory.Spectrum.Prime.Topology -import Mathlib.Order.SuccPred.WithBot - -/-! -# Constructible sets in the prime spectrum - -This file provides tooling for manipulating constructible sets in the prime spectrum of a ring. - -## TODO - -Link to constructible sets in a topological space. --/ - -open Finset -open scoped Polynomial - -namespace PrimeSpectrum -variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T] - -variable (R) in -/-- The data of a constructible set `s` is finitely many tuples `(f, g₁, ..., gₙ)` such that -`s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f)`. - -To obtain `s` from its data, use `PrimeSpectrum.ConstructibleSetData.toSet`. -/ -abbrev ConstructibleSetData := Finset (Σ n, R × (Fin n → R)) - -namespace ConstructibleSetData - -/-- Given the data of the constructible set `s`, build the data of the constructible set -`{I | {x | f x ∈ I} ∈ s}`. -/ -def map [DecidableEq S] (f : R →+* S) (s : ConstructibleSetData R) : ConstructibleSetData S := - s.image <| Sigma.map id fun _n (r, g) ↦ (f r, f ∘ g) - -@[simp] lemma map_id [DecidableEq R] (s : ConstructibleSetData R) : s.map (.id _) = s := by - unfold map Sigma.map; simp [RingHom.coe_id] - -lemma map_comp [DecidableEq S] [DecidableEq T] (f : S →+* T) (g : R →+* S) - (s : ConstructibleSetData R) : s.map (f.comp g) = (s.map g).map f := by - unfold map Sigma.map; simp [image_image, Function.comp_def] - -/-- Given the data of a constructible set `s`, namely finitely many tuples `(f, g₁, ..., gₙ)` such -that `s = ⋃ (f, g₁, ..., gₙ), V(g₁, ..., gₙ) \ V(f)`, return `s`. -/ -def toSet (S : ConstructibleSetData R) : Set (PrimeSpectrum R) := - ⋃ x ∈ S, zeroLocus (Set.range x.2.2) \ zeroLocus {x.2.1} - -@[simp] -lemma toSet_map [DecidableEq S] (f : R →+* S) (s : ConstructibleSetData R) : - (s.map f).toSet = comap f ⁻¹' s.toSet := by - unfold toSet map - rw [set_biUnion_finset_image] - simp only [id_eq, Set.preimage_iUnion, Set.preimage_diff, preimage_comap_zeroLocus, - Set.image_singleton, ← Set.range_comp] - rfl - -/-- The degree bound on a constructible set for Chevalley's theorem for the inclusion `R ↪ R[X]`. -/ -def degBound (S : ConstructibleSetData R[X]) : ℕ := S.sup fun e ↦ ∑ i, (e.2.2 i).degree.succ - -end PrimeSpectrum.ConstructibleSetData diff --git a/LeanCamCombi/GrowthInGroups/Lecture2.lean b/LeanCamCombi/GrowthInGroups/Lecture2.lean index 1a20f1a873..91e767df46 100644 --- a/LeanCamCombi/GrowthInGroups/Lecture2.lean +++ b/LeanCamCombi/GrowthInGroups/Lecture2.lean @@ -1,5 +1,5 @@ import Mathlib.Algebra.Order.Group.Pointwise.Interval -import LeanCamCombi.GrowthInGroups.ApproximateSubgroup +import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup open Fin Finset List open scoped Pointwise diff --git a/LeanCamCombi/GrowthInGroups/Lecture3.lean b/LeanCamCombi/GrowthInGroups/Lecture3.lean index b7a0871a66..1f9caaa0ee 100644 --- a/LeanCamCombi/GrowthInGroups/Lecture3.lean +++ b/LeanCamCombi/GrowthInGroups/Lecture3.lean @@ -1,5 +1,5 @@ import Mathlib.Geometry.Group.Growth.QuotientInter -import LeanCamCombi.GrowthInGroups.ApproximateSubgroup +import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup open Finset open scoped Pointwise diff --git a/LeanCamCombi/GrowthInGroups/Lecture4.lean b/LeanCamCombi/GrowthInGroups/Lecture4.lean index 124f2f97d9..43b76dcfa9 100644 --- a/LeanCamCombi/GrowthInGroups/Lecture4.lean +++ b/LeanCamCombi/GrowthInGroups/Lecture4.lean @@ -1,7 +1,7 @@ import Mathlib.Analysis.Matrix import Mathlib.GroupTheory.Nilpotent import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs -import LeanCamCombi.GrowthInGroups.ApproximateSubgroup +import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup import LeanCamCombi.Util open Group diff --git a/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Basic.lean b/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Basic.lean deleted file mode 100644 index 82d16abea9..0000000000 --- a/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Basic.lean +++ /dev/null @@ -1,38 +0,0 @@ -import Mathlib.Algebra.MvPolynomial.Basic - -namespace Submodule -variable {R S σ : Type*} [CommSemiring R] [CommSemiring S] - -section Module -variable [Module R S] {M N : Submodule R S} {x : MvPolynomial σ S} - -variable (σ M) -@[simps] -def mvPolynomial : Submodule R (MvPolynomial σ S) where - carrier := {p | ∀ i, p.coeff i ∈ M} - add_mem' := by simp+contextual [add_mem] - zero_mem' := by simp - smul_mem' := by simp+contextual [Submodule.smul_mem] - -@[simp] lemma mem_mvPolynomial : x ∈ M.mvPolynomial σ ↔ ∀ i, x.coeff i ∈ M := .rfl - -end Module - -section Algebra -variable [Algebra R S] {M N : Submodule R S} {x : MvPolynomial σ S} {n : ℕ} - -lemma le_mvPolynomial_mul : M.mvPolynomial σ * N.mvPolynomial σ ≤ (M * N).mvPolynomial σ := by - classical - rw [mul_le] - intros x hx y hy k - rw [MvPolynomial.coeff_mul] - exact sum_mem fun c hc ↦ mul_mem_mul (hx _) (hy _) - -lemma mvPolynomial_pow_le : M.mvPolynomial σ ^ n ≤ (M ^ n).mvPolynomial σ := by - classical - induction' n with n IH - · simpa [MvPolynomial.coeff_one, apply_ite] using ⟨1, map_one _⟩ - · exact (Submodule.mul_le_mul_left IH).trans le_mvPolynomial_mul - -end Algebra -end Submodule diff --git a/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Degrees.lean b/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Degrees.lean index f3db35ed77..a1abf24ea9 100644 --- a/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Degrees.lean +++ b/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Degrees.lean @@ -3,23 +3,16 @@ import Mathlib.Algebra.MvPolynomial.Degrees namespace MvPolynomial variable {R σ : Type*} [CommSemiring R] {m n : Multiset σ} {p : MvPolynomial σ R} -lemma degrees_map_le {σ S} [CommSemiring S] (p : MvPolynomial σ R) (f : R →+* S) : - (MvPolynomial.map f p).degrees ≤ p.degrees := by - classical - dsimp only [MvPolynomial.degrees] - apply Finset.sup_mono - apply MvPolynomial.support_map_subset - variable (R σ n) in def degreesLE : Submodule R (MvPolynomial σ R) where carrier := {p | p.degrees ≤ n} - add_mem' {a b} ha hb := by classical exact (MvPolynomial.degrees_add a b).trans (sup_le ha hb) + add_mem' {a b} ha hb := by classical exact degrees_add_le.trans (sup_le ha hb) zero_mem' := by simp smul_mem' c {x} hx := by dsimp rw [Algebra.smul_def] - refine (MvPolynomial.degrees_mul _ _).trans ?_ - simpa [MvPolynomial.degrees_C] using hx + refine degrees_mul_le.trans ?_ + simpa [degrees_C] using hx @[simp] lemma mem_degreesLE : p ∈ degreesLE R σ n ↔ p.degrees ≤ n := Iff.rfl @@ -27,8 +20,7 @@ lemma degreesLE_mul : degreesLE R σ m * degreesLE R σ n = degreesLE R σ (m + classical apply le_antisymm · rw [Submodule.mul_le] - intro x hx y hy - exact (degrees_mul _ _).trans (add_le_add hx hy) + exact fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy) · intro x hx rw [x.as_sum] refine sum_mem fun i hi ↦ ?_ diff --git a/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Equiv.lean b/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Equiv.lean deleted file mode 100644 index 688afa20fc..0000000000 --- a/LeanCamCombi/Mathlib/Algebra/MvPolynomial/Equiv.lean +++ /dev/null @@ -1,33 +0,0 @@ -import Mathlib.Algebra.MvPolynomial.Equiv - -namespace MvPolynomial -variable {R σ : Type*} [CommSemiring R] [IsEmpty σ] - -@[simp] lemma isEmptyRingEquiv_toRingHom : (isEmptyRingEquiv R σ).symm.toRingHom = C := rfl -@[simp] lemma isEmptyRingEquiv_symm_apply (r : R) : (isEmptyRingEquiv R σ).symm r = C r := rfl - -lemma isEmptyRingEquiv_eq_coeff_zero {σ R : Type*} [CommSemiring R] [IsEmpty σ] {x} : - isEmptyRingEquiv R σ x = x.coeff 0 := by - obtain ⟨x, rfl⟩ := (isEmptyRingEquiv R σ).symm.surjective x - simp - -noncomputable -def commAlgEquiv (R S₁ S₂ : Type*) [CommSemiring R] : - MvPolynomial S₁ (MvPolynomial S₂ R) ≃ₐ[R] MvPolynomial S₂ (MvPolynomial S₁ R) := - (sumAlgEquiv R S₁ S₂).symm.trans ((renameEquiv _ (.sumComm S₁ S₂)).trans (sumAlgEquiv R S₂ S₁)) - -lemma commAlgEquiv_C {R S₁ S₂ : Type*} [CommSemiring R] (p) : - commAlgEquiv R S₁ S₂ (.C p) = .map C p := by - suffices (commAlgEquiv R S₁ S₂).toAlgHom.comp - (IsScalarTower.toAlgHom R (MvPolynomial S₂ R) _) = mapAlgHom (Algebra.ofId _ _) by - exact DFunLike.congr_fun this p - ext x : 1 - simp [commAlgEquiv] - -lemma commAlgEquiv_C_X {R S₁ S₂ : Type*} [CommSemiring R] (i) : - commAlgEquiv R S₁ S₂ (.C (.X i)) = .X i := by simp [commAlgEquiv_C] - -lemma commAlgEquiv_X {R S₁ S₂ : Type*} [CommSemiring R] (i) : - commAlgEquiv R S₁ S₂ (.X i) = .C (.X i) := by simp [commAlgEquiv] - -end MvPolynomial diff --git a/LeanCamCombi/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean b/LeanCamCombi/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean new file mode 100644 index 0000000000..c226e0dcb6 --- /dev/null +++ b/LeanCamCombi/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean @@ -0,0 +1,60 @@ +import Mathlib.Algebra.Order.BigOperators.Ring.Finset +import Mathlib.Combinatorics.Additive.ApproximateSubgroup +import Mathlib.Tactic.Bound + +open scoped Finset Pointwise + +variable {G : Type*} [Group G] {A B : Set G} {K L : ℝ} {m n : ℕ} + +namespace IsApproximateSubgroup + +@[to_additive] +lemma pi {ι : Type*} {G : ι → Type*} [Fintype ι] [∀ i, Group (G i)] {A : ∀ i, Set (G i)} {K : ι → ℝ} + (hA : ∀ i, IsApproximateSubgroup (K i) (A i)) : + IsApproximateSubgroup (∏ i, K i) (Set.univ.pi A) where + one_mem i _ := (hA i).one_mem + inv_eq_self := by simp [(hA _).inv_eq_self] + sq_covBySMul := by + choose F hF hFS using fun i ↦ (hA i).sq_covBySMul + classical + refine ⟨Fintype.piFinset F, ?_, ?_⟩ + · calc + #(Fintype.piFinset F) = ∏ i, (#(F i) : ℝ) := by simp + _ ≤ ∏ i, K i := by gcongr; exact hF _ + · sorry + +end IsApproximateSubgroup + +open Finset in +open scoped RightActions in +@[to_additive] +lemma exists_isApproximateSubgroup_of_small_doubling [DecidableEq G] {A : Finset G} + (hA₀ : A.Nonempty) (hA : #(A ^ 2) ≤ K * #A) : + ∃ S ⊆ (A⁻¹ * A) ^ 2, IsApproximateSubgroup (2 ^ 12 * K ^ 36) (S : Set G) ∧ + #S ≤ 16 * K ^ 12 * #A ∧ ∃ a ∈ A, #A / (2 * K) ≤ #(A ∩ S <• a) := by + have hK : 1 ≤ K := one_le_of_le_mul_right₀ (by positivity) <| + calc (#A : ℝ) ≤ #(A ^ 2) := mod_cast card_le_card_pow two_ne_zero + _ ≤ K * #A := hA + let S : Finset G := {g ∈ A⁻¹ * A | #A / (2 * K) ≤ #(A <• g ∩ A)} + have hS₁ : 1 ∈ S := by simp [S, hA₀.ne_empty]; bound + have hS₀ : S.Nonempty := ⟨1, hS₁⟩ + have hSA : S ⊆ A⁻¹ * A := filter_subset .. + have hSsymm : S⁻¹ = S := by ext; simp [S]; simp [← mem_inv']; sorry + have hScard := calc + (#S : ℝ) ≤ #(A⁻¹ * A) := by gcongr + _ ≤ K ^ 2 * #A := sorry + obtain ⟨F, hFA, hFcard, hASF⟩ : ∃ F ⊆ A, #F ≤ 2 * K ∧ A ⊆ S * F := sorry + refine ⟨S ^ 2, by gcongr, ?_, ?_, ?_⟩ + · rw [show 2 ^ 12 * K ^ 36 = (2 ^ 4 * K ^ 12) ^ 3 by ring, coe_pow] + refine .of_small_tripling hS₁ hSsymm ?_ + calc + (#(S ^ 3) : ℝ) + _ ≤ #(A * S ^ 3) := mod_cast card_le_card_mul_left hA₀ + _ ≤ #(A * S ^ 3 * A⁻¹) := mod_cast card_le_card_mul_right hA₀.inv + _ ≤ 8 * K ^ 11 * #A := sorry + _ ≤ 8 * K ^ 11 * #(S * F) := by gcongr + _ ≤ 8 * K ^ 11 * (#S * #F) := by gcongr; exact mod_cast card_mul_le + _ ≤ 8 * K ^ 11 * (#S * (2 * K)) := by gcongr + _ = 2 ^ 4 * K ^ 12 * #S := by ring + sorry + sorry diff --git a/LeanCamCombi/Mathlib/Data/List/DropRight.lean b/LeanCamCombi/Mathlib/Data/List/DropRight.lean index 046bab3d1e..7b01fca3b5 100644 --- a/LeanCamCombi/Mathlib/Data/List/DropRight.lean +++ b/LeanCamCombi/Mathlib/Data/List/DropRight.lean @@ -1,7 +1,4 @@ -import Batteries.Data.List.Perm import Mathlib.Data.List.DropRight -import Mathlib.Data.List.Infix -import Mathlib.Data.Nat.Defs namespace List variable {α : Type*} {l l' l₀ l₁ l₂ : List α} {a b : α} {m n : ℕ} diff --git a/LeanCamCombi/Mathlib/Data/Set/Image.lean b/LeanCamCombi/Mathlib/Data/Set/Image.lean deleted file mode 100644 index 3f59989249..0000000000 --- a/LeanCamCombi/Mathlib/Data/Set/Image.lean +++ /dev/null @@ -1,13 +0,0 @@ -import Mathlib.Data.Set.Image - -namespace Set -variable {α β γ γ₁ γ₂ δ δ₁ δ₂ : Type*} {h : β → α} {f : γ → β} {f₁ : γ₁ → α} {f₂ : γ → γ₁} - {g : δ → β} {g₁ : δ₁ → α} {g₂ : δ → δ₁} - -lemma image_of_range_union_range_eq_univ (hf : h ∘ f = f₁ ∘ f₂) (hg : h ∘ g = g₁ ∘ g₂) - (hfg : range f ∪ range g = univ) (s : Set β) : - h '' s = f₁ '' (f₂ '' (f ⁻¹' s)) ∪ g₁ '' (g₂ '' (g ⁻¹' s)) := by - rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range, - image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ] - -end Set diff --git a/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean b/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean index 3a623a40a2..9109e7fdd3 100644 --- a/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean +++ b/LeanCamCombi/Mathlib/Data/Set/Pointwise/SMul.lean @@ -17,16 +17,3 @@ lemma mul_singleton' (s : Set α) (a : α) : s * {a} = op a • s := mul_singlet end Mul end Set - -namespace Set -variable {α β : Type*} - -section Group -variable [Group α] [MulAction α β] {s : Set β} {t : Set β} {a : α} - --- TODO: Replace -@[to_additive (attr := simp)] -lemma smul_set_subset_smul_set_iff : a • s ⊆ a • t ↔ s ⊆ t := set_smul_subset_set_smul_iff - -end Group -end Set diff --git a/LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean b/LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean index d8c4f54297..06a3878feb 100644 --- a/LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean +++ b/LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean @@ -3,9 +3,6 @@ import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic /-! # TODO -* Golf `condExp_const`, no `@` -* Remove useless `haveI`/`letI` -* Make `m` explicit in `condExp_add`, `condExp_sub`, etc... * See https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Conditional.20expectation.20of.20product for how to prove that we can pull `m`-measurable continuous linear maps out of the `m`-conditional expectation. @@ -30,34 +27,3 @@ lemma condExp_ofNat (n : ℕ) [n.AtLeastTwo] (f : Ω → R) : simpa [Nat.cast_smul_eq_nsmul] using condExp_smul (μ := μ) (m := m) (n : ℝ) f end NormedRing - -variable [IsFiniteMeasure μ] [InnerProductSpace ℝ E] - -lemma Memℒp.condExpL2_ae_eq_condExp (hm : m ≤ m₀) (hf : Memℒp f 2 μ) : - condExpL2 E ℝ hm hf.toLp =ᵐ[μ] μ[f | m] := by - refine ae_eq_condExp_of_forall_setIntegral_eq hm - (memℒp_one_iff_integrable.1 <| hf.mono_exponent one_le_two) - (fun s hs htop ↦ integrableOn_condExpL2_of_measure_ne_top hm htop.ne _) (fun s hs htop ↦ ?_) - (aeStronglyMeasurable'_condExpL2 hm _) - rw [integral_condExpL2_eq hm (hf.toLp _) hs htop.ne] - refine setIntegral_congr_ae (hm _ hs) ?_ - filter_upwards [hf.coeFn_toLp] with ω hω _ using hω - -lemma eLpNorm_condExp_le : eLpNorm (μ[f | m]) 2 μ ≤ eLpNorm f 2 μ := by - by_cases hm : m ≤ m₀; swap - · simp [condExp_of_not_le hm] - by_cases hfm : AEStronglyMeasurable f μ; swap - · rw [condExp_undef (by simp [Integrable, not_and_of_not_left _ hfm])] - simp - obtain hf | hf := eq_or_ne (eLpNorm f 2 μ) ∞ - · simp [hf] - replace hf : Memℒp f 2 μ := ⟨hfm, Ne.lt_top' fun a ↦ hf (id (Eq.symm a))⟩ - rw [← eLpNorm_congr_ae (hf.condExpL2_ae_eq_condExp hm)] - refine le_trans (eLpNorm_condExpL2_le hm _) ?_ - rw [eLpNorm_congr_ae hf.coeFn_toLp] - -protected lemma Memℒp.condExp (hf : Memℒp f 2 μ) : Memℒp (μ[f | m]) 2 μ := by - by_cases hm : m ≤ m₀ - · exact ⟨(stronglyMeasurable_condExp.mono hm).aestronglyMeasurable, - eLpNorm_condExp_le.trans_lt hf.eLpNorm_lt_top⟩ - · simp [condExp_of_not_le hm] diff --git a/LeanCamCombi/Mathlib/Order/RelIso/Group.lean b/LeanCamCombi/Mathlib/Order/RelIso/Group.lean index 1eda29e2a4..19fc5d1cdc 100644 --- a/LeanCamCombi/Mathlib/Order/RelIso/Group.lean +++ b/LeanCamCombi/Mathlib/Order/RelIso/Group.lean @@ -1,35 +1,26 @@ +import Mathlib.Algebra.Group.Action.Faithful import Mathlib.Algebra.Group.Opposite -import Mathlib.GroupTheory.GroupAction.Defs import Mathlib.Order.RelIso.Group namespace RelIso - variable {α : Type*} {r : α → α → Prop} /-- The tautological action by `r ≃r r` on `α`. -/ -instance applyMulAction : MulAction (r ≃r r) α - where +instance applyMulAction : MulAction (r ≃r r) α where smul := (⇑) one_smul _ := rfl mul_smul _ _ _ := rfl /-- The tautological action by `r ≃r r` on `α`. -/ -instance applyOpMulAction : MulAction (r ≃r r)ᵐᵒᵖ α - where +instance applyOpMulAction : MulAction (r ≃r r)ᵐᵒᵖ α where smul e := e.unop.symm one_smul _ := rfl mul_smul _ _ _ := rfl -@[simp] -theorem smul_def (f : r ≃r r) (a : α) : f • a = f a := - rfl - -@[simp] -theorem op_smul_def (f : (r ≃r r)ᵐᵒᵖ) (a : α) : f • a = f.unop.symm a := - rfl +@[simp] lemma smul_def (f : r ≃r r) (a : α) : f • a = f a := rfl +@[simp] lemma op_smul_def (f : (r ≃r r)ᵐᵒᵖ) (a : α) : f • a = f.unop.symm a := rfl -instance apply_faithfulSMul : FaithfulSMul (r ≃r r) α where - eq_of_smul_eq_smul h := RelIso.ext h +instance apply_faithfulSMul : FaithfulSMul (r ≃r r) α where eq_of_smul_eq_smul h := RelIso.ext h instance apply_op_faithfulSMul : FaithfulSMul (r ≃r r)ᵐᵒᵖ α := sorry diff --git a/LeanCamCombi/Mathlib/RingTheory/Spectrum/Prime/Topology.lean b/LeanCamCombi/Mathlib/RingTheory/Spectrum/Prime/Topology.lean deleted file mode 100644 index 8ccd4617ae..0000000000 --- a/LeanCamCombi/Mathlib/RingTheory/Spectrum/Prime/Topology.lean +++ /dev/null @@ -1,28 +0,0 @@ -import Mathlib.RingTheory.Localization.Algebra -import Mathlib.RingTheory.Spectrum.Prime.Topology - -variable {R S : Type*} [CommSemiring R] [CommSemiring S] - -namespace PrimeSpectrum - -lemma coe_comap (f : R →+* S) : comap f = f.specComap := rfl - -lemma comap_apply (f : R →+* S) (x) : comap f x = f.specComap x := rfl - -open Localization Polynomial Set - -variable {R : Type*} [CommRing R] (c : R) - -lemma range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk (c : R) : - letI := (mapRingHom (algebraMap R (Away c))).toAlgebra - (range (comap (algebraMap R[X] (Away c)[X])))ᶜ - = range (comap (mapRingHom (Ideal.Quotient.mk (.span {c})))) := by - letI := (mapRingHom (algebraMap R (Away c))).toAlgebra - have := Polynomial.isLocalization (.powers c) (Away c) - rw [Submonoid.map_powers] at this - have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span {c}))) := - Polynomial.map_surjective _ Ideal.Quotient.mk_surjective - rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)] - simp [Polynomial.ker_mapRingHom, Ideal.map_span] - -end PrimeSpectrum diff --git a/LeanCamCombi/PhD/VCDim/CondVar.lean b/LeanCamCombi/PhD/VCDim/CondVar.lean index 72c5dd7a90..38c5a5e34a 100644 --- a/LeanCamCombi/PhD/VCDim/CondVar.lean +++ b/LeanCamCombi/PhD/VCDim/CondVar.lean @@ -126,10 +126,10 @@ lemma condVar_ae_eq_condExp_sq_sub_condExp_sq (hm : m ≤ m₀) [IsFiniteMeasure rw [(_ : 2 * X * μ[X|m] = fun ω ↦ 2 * (X ω * (μ[X|m]) ω))] swap; ext ω; simp [mul_assoc] have aux₁' : Memℒp (X * μ[X | m]) 1 μ := by - refine @Memℒp.mul Ω m₀ _ _ _ 1 2 2 _ _ hX.condExp hX ?_ + refine @Memℒp.mul _ m₀ _ _ _ _ _ 2 _ _ (hX.condExp (𝕜 := ℝ)) hX ?_ simp [ENNReal.inv_two_add_inv_two] exact Integrable.const_mul (memℒp_one_iff_integrable.1 aux₁') (2 : ℝ) - have aux₂ : Integrable (μ[X|m] ^ 2) μ := hX.condExp.integrable_sq + have aux₂ : Integrable (μ[X|m] ^ 2) μ := (hX.condExp (𝕜 := ℝ)).integrable_sq filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁, condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁ ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X] @@ -153,10 +153,10 @@ lemma integral_condVar_add_variance_condExp (hm : m ≤ m₀) [IsProbabilityMeas _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by congr 1 · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_condExp_sq hm hX - · exact variance_def' hX.condExp + · exact variance_def' (hX.condExp (𝕜 := ℝ)) _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm] - exact hX.condExp.integrable_sq + exact (hX.condExp (𝕜 := ℝ)).integrable_sq _ = Var[X ; μ] := by rw [variance_def' hX]; ring lemma condVar_bot' [NeZero μ] (X : Ω → ℝ) : diff --git a/README.md b/README.md index 09c9c23d38..75a0e1640f 100644 --- a/README.md +++ b/README.md @@ -47,7 +47,6 @@ The following topics are under active development in LeanCamCombi. * The Birkhoff representation theorem, categorical version * The Minkowski-Carathéodory theorem * Approximate subgroups -* Chevalley's theorem about constructible sets * Model theoretic stability and its relation to additive combinatorics See the [upstreaming dashboard](https://yaeldillies.github.io/LeanCamCombi/upstreaming) for more information. @@ -59,6 +58,7 @@ The following topics are covered in LeanCamCombi and could be upstreamed to Math * Kneser's addition theorem * The Sylvester-Chvatal theorem * Containment of graphs +* Chevalley's theorem about constructible sets with complexity bound See the [upstreaming dashboard](https://yaeldillies.github.io/LeanCamCombi/upstreaming) for more information. @@ -82,6 +82,8 @@ The following topics have been upstreamed to mathlib and no longer live in LeanC * Visibility of a point through a set * The upper bound on the Ruzsa-Szemerédi problem * Cauchy's functional equation +* Chevalley's theorem about constructible sets without complexity bound +* Marked groups ## Interacting with the project diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json index 190c0606da..7bce9939b7 100644 --- a/docbuild/lake-manifest.json +++ b/docbuild/lake-manifest.json @@ -62,7 +62,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fc30cf7d2a282e7e1e29be801db327f1f52004e7", + "rev": "fb8b7ee74e32f1ece9601ed397153089bcadb2c1", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lake-manifest.json b/lake-manifest.json index 58391fe8bc..cbdbb50afe 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "fc30cf7d2a282e7e1e29be801db327f1f52004e7", + "rev": "fb8b7ee74e32f1ece9601ed397153089bcadb2c1", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,