Clean Chevalley up

Author: YaelDillies

LeanCamCombi.lean

@@ -12,21 +12,32 @@ import LeanCamCombi.GraphTheory.ExampleSheet1
 import LeanCamCombi.GraphTheory.ExampleSheet2
 import LeanCamCombi.GrowthInGroups.ApproximateSubgroup
 import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
+import LeanCamCombi.GrowthInGroups.CharPolyBaseChange
 import LeanCamCombi.GrowthInGroups.Chevalley
+import LeanCamCombi.GrowthInGroups.ChevalleyComplex
 import LeanCamCombi.GrowthInGroups.Constructible
+import LeanCamCombi.GrowthInGroups.ConstructiblePrimeSpectrum
 import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
+import LeanCamCombi.GrowthInGroups.PolynomialLocalization
+import LeanCamCombi.GrowthInGroups.PrimeSpectrumPolynomial
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
 import LeanCamCombi.Impact
 import LeanCamCombi.Incidence
 import LeanCamCombi.Kneser.Kneser
 import LeanCamCombi.Kneser.KneserRuzsa
 import LeanCamCombi.Kneser.MulStab
 import LeanCamCombi.LittlewoodOfford
+import LeanCamCombi.Mathlib.Algebra.Algebra.Operations
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
 import LeanCamCombi.Mathlib.Algebra.Group.Subgroup.Pointwise
+import LeanCamCombi.Mathlib.Algebra.Order.GroupWithZero.Unbundled
+import LeanCamCombi.Mathlib.Algebra.Polynomial.Degree.Lemmas
+import LeanCamCombi.Mathlib.Algebra.Polynomial.Div
+import LeanCamCombi.Mathlib.Algebra.Polynomial.Eval
+import LeanCamCombi.Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
 import LeanCamCombi.Mathlib.Analysis.Convex.Exposed
 import LeanCamCombi.Mathlib.Analysis.Convex.Extreme
 import LeanCamCombi.Mathlib.Analysis.Convex.Independence
@@ -43,6 +54,7 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 import LeanCamCombi.Mathlib.Data.Finset.Basic
 import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
+import LeanCamCombi.Mathlib.Data.Fintype.Card
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
@@ -55,9 +67,13 @@ import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
 import LeanCamCombi.Mathlib.Order.Interval.Finset.Defs
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
+import LeanCamCombi.Mathlib.Order.RelClasses
 import LeanCamCombi.Mathlib.Order.SupClosed
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
+import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Ideal.Span
+import LeanCamCombi.Mathlib.RingTheory.LocalRing.ResidueField.Ideal
+import LeanCamCombi.Mathlib.RingTheory.Polynomial.Basic
 import LeanCamCombi.Mathlib.Topology.Defs.Induced
 import LeanCamCombi.Mathlib.Topology.Spectral.Hom
 import LeanCamCombi.MetricBetween

LeanCamCombi/GrowthInGroups/CharPolyBaseChange.lean

@@ -0,0 +1,20 @@
+import Mathlib.LinearAlgebra.Charpoly.ToMatrix
+import Mathlib.RingTheory.TensorProduct.Free
+
+open Polynomial TensorProduct
+
+universe u v
+variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
+
+lemma LinearMap.charpoly_baseChange [Module.Free R M] [Module.Finite R M]
+    {A} [CommRing A] [Algebra R A] (f : M →ₗ[R] M) :
+    (f.baseChange A).charpoly = f.charpoly.map (algebraMap R A) := by
+  nontriviality A
+  have := (algebraMap R A).domain_nontrivial
+  let I := Module.Free.ChooseBasisIndex R M
+  let b : Basis I R M := Module.Free.chooseBasis R M
+  rw [← f.charpoly_toMatrix b, ← (f.baseChange A).charpoly_toMatrix (b.baseChange A),
+    ← Matrix.charpoly_map]
+  congr 1
+  ext i j
+  simp [Matrix.map_apply, LinearMap.toMatrix_apply, ← Algebra.algebraMap_eq_smul_one]