feat: basic theory connecting R[X]-submodules and invariant R-sub…

…modules (#9721)

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -317,6 +317,28 @@ theorem mem_sSup_of_mem {S : Set (Submodule R M)} {s : Submodule R M} (hs : s 
   exact this
 #align submodule.mem_Sup_of_mem Submodule.mem_sSup_of_mem
 
+@[simp]
+theorem toAddSubmonoid_sSup (s : Set (Submodule R M)) :
+    (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s) := by
+  let p : Submodule R M :=
+    { toAddSubmonoid := sSup (toAddSubmonoid '' s)
+      smul_mem' := fun t {m} h ↦ by
+        simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢
+        refine AddSubmonoid.iSup_induction'
+          (C := fun x _ ↦ t • x ∈ ⨆ p : toAddSubmonoid '' s, (p : AddSubmonoid M)) ?_ ?_
+          (fun x y _ _ ↦ ?_) h
+        · rintro ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ x (hx : x ∈ p)
+          suffices p.toAddSubmonoid ≤ ⨆ q : toAddSubmonoid '' s, (q : AddSubmonoid M) by
+            exact this (smul_mem p t hx)
+          apply le_sSup
+          rw [Subtype.range_coe_subtype]
+          exact ⟨p, hp, rfl⟩
+        · simpa only [smul_zero] using zero_mem _
+        · simp_rw [smul_add]; exact add_mem }
+  refine le_antisymm (?_ : sSup s ≤ p) ?_
+  · exact sSup_le fun q hq ↦ le_sSup <| Set.mem_image_of_mem toAddSubmonoid hq
+  · exact sSup_le fun _ ⟨q, hq, hq'⟩ ↦ hq'.symm ▸ le_sSup hq
+
 variable (R)
 
 @[simp]

Mathlib/Algebra/Module/Submodule/RestrictScalars.lean

@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Andre
   Johannes Hölzl, Kevin Buzzard, Yury Kudryashov
 -/
 import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Order.Hom.CompleteLattice
 
 /-!
 
@@ -116,4 +117,11 @@ theorem restrictScalars_eq_top_iff {p : Submodule R M} : restrictScalars S p = 
   simp [SetLike.ext_iff]
 #align submodule.restrict_scalars_eq_top_iff Submodule.restrictScalars_eq_top_iff
 
+/-- If ring `S` acts on a ring `R` and `M` is a module over both (compatibly with this action) then
+we can turn an `R`-submodule into an `S`-submodule by forgetting the action of `R`. -/
+def restrictScalarsLatticeHom : CompleteLatticeHom (Submodule R M) (Submodule S M) where
+  toFun := restrictScalars S
+  map_sInf' s := by ext; simp
+  map_sSup' s := by rw [← toAddSubmonoid_eq, toAddSubmonoid_sSup, ← Set.image_comp]; simp
+
 end Submodule

Mathlib/Data/Polynomial/AlgebraMap.lean

@@ -534,4 +534,28 @@ theorem aeval_endomorphism {M : Type*} [CommRing R] [AddCommGroup M] [Module R M
   exact map_sum (LinearMap.applyₗ v) _ _
 #align polynomial.aeval_endomorphism Polynomial.aeval_endomorphism
 
+section StableSubmodule
+
+variable {M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
+  {q : Submodule R M} {m : M} (hm : m ∈ q) (p : R[X])
+
+lemma aeval_apply_smul_mem_of_le_comap'
+    [Semiring A] [Algebra R A] [Module A M] [IsScalarTower R A M] (a : A)
+    (hq : q ≤ q.comap (Algebra.lsmul R R M a)) :
+    aeval a p • m ∈ q := by
+  refine p.induction_on (M := fun f ↦ aeval a f • m ∈ q) (by simpa) (fun f₁ f₂ h₁ h₂ ↦ ?_)
+    (fun n t hmq ↦ ?_)
+  · simp_rw [map_add, add_smul]
+    exact Submodule.add_mem q h₁ h₂
+  · dsimp only at hmq ⊢
+    rw [pow_succ, mul_left_comm, map_mul, aeval_X, mul_smul]
+    rw [← q.map_le_iff_le_comap] at hq
+    exact hq ⟨_, hmq, rfl⟩
+
+lemma aeval_apply_smul_mem_of_le_comap (f : Module.End R M) (hq : q ≤ q.comap f) :
+    aeval f p m ∈ q :=
+  aeval_apply_smul_mem_of_le_comap' hm p f hq
+
+end StableSubmodule
+
 end Polynomial

Mathlib/Data/Polynomial/Module.lean

@@ -69,6 +69,9 @@ lemma of_aeval_smul (f : R[X]) (m : M) : of R M a (aeval a f • m) = f • of R
 @[simp] lemma of_symm_smul (f : R[X]) (m : AEval R M a) :
     (of R M a).symm (f • m) = aeval a f • (of R M a).symm m := rfl
 
+@[simp] lemma C_smul (t : R) (m : AEval R M a) : C t • m = t • m :=
+  (of R M a).symm.injective <| by simp
+
 lemma X_smul_of (m : M) : (X : R[X]) • (of R M a m) = of R M a (a • m) := by
   rw [← of_aeval_smul, aeval_X]
 
@@ -79,12 +82,57 @@ lemma of_symm_X_smul (m : AEval R M a) :
 instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a where
   smul_assoc r f m := by
     apply (of R M a).symm.injective
-    rw [of_symm_smul, map_smul, smul_assoc]
-    rfl
+    rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]
 
 instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a :=
   Finite.of_restrictScalars_finite R _ _
 
+section Submodule
+
+variable {p : Submodule R M} (hp : p ≤ p.comap (Algebra.lsmul R R M a))
+  {q : Submodule R[X] <| AEval R M a}
+
+variable (R M) in
+/-- We can turn an `R[X]`-submodule into an `R`-submodule by forgetting the action of `X`. -/
+def comapSubmodule :
+    CompleteLatticeHom (Submodule R[X] <| AEval R M a) (Submodule R M) :=
+  (Submodule.orderIsoMapComap (of R M a)).symm.toCompleteLatticeHom.comp <|
+    Submodule.restrictScalarsLatticeHom R R[X] (AEval R M a)
+
+@[simp] lemma mem_comapSubmodule {x : M} :
+    x ∈ comapSubmodule R M a q ↔ of R M a x ∈ q :=
+  Iff.rfl
+
+@[simp] lemma comapSubmodule_le_comap :
+    comapSubmodule R M a q ≤ (comapSubmodule R M a q).comap (Algebra.lsmul R R M a) := by
+  intro m hm
+  simpa only [Submodule.mem_comap, Algebra.lsmul_coe, mem_comapSubmodule, ← X_smul_of] using
+    q.smul_mem (X : R[X]) hm
+
+/-- An `R`-submodule which is stable under the action of `a` can be promoted to an
+`R[X]`-submodule. -/
+def mapSubmodule : Submodule R[X] <| AEval R M a :=
+  { toAddSubmonoid := p.toAddSubmonoid.map (of R M a)
+    smul_mem' := by
+      rintro f - ⟨m : M, h : m ∈ p, rfl⟩
+      simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, AddSubmonoid.mem_map,
+        Submodule.mem_toAddSubmonoid]
+      exact ⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a hp, of_aeval_smul a f m⟩ }
+
+@[simp] lemma mem_mapSubmodule {m : AEval R M a} :
+    m ∈ mapSubmodule a hp ↔ (of R M a).symm m ∈ p :=
+  ⟨fun ⟨_, hm, hm'⟩ ↦ hm'.symm ▸ hm, fun hm ↦ ⟨(of R M a).symm m, hm, rfl⟩⟩
+
+@[simp] lemma mapSubmodule_comapSubmodule (h := comapSubmodule_le_comap a) :
+    mapSubmodule a (p := comapSubmodule R M a q) h = q := by
+  ext; simp
+
+@[simp] lemma comapSubmodule_mapSubmodule :
+    comapSubmodule R M a (mapSubmodule a hp) = p := by
+  ext; simp
+
+end Submodule
+
 end AEval
 
 variable (φ : M →ₗ[R] M)

Mathlib/Order/Hom/CompleteLattice.lean

@@ -218,6 +218,13 @@ instance (priority := 100) OrderIsoClass.toCompleteLatticeHomClass [CompleteLatt
   { OrderIsoClass.tosSupHomClass, OrderIsoClass.tosInfHomClass with }
 #align order_iso_class.to_complete_lattice_hom_class OrderIsoClass.toCompleteLatticeHomClass
 
+/-- Reinterpret an order isomorphism as a morphism of complete lattices. -/
+@[simps] def OrderIso.toCompleteLatticeHom [CompleteLattice α] [CompleteLattice β]
+    (f : OrderIso α β) : CompleteLatticeHom α β where
+  toFun := f
+  map_sInf' := sInfHomClass.map_sInf f
+  map_sSup' := sSupHomClass.map_sSup f
+
 instance [SupSet α] [SupSet β] [sSupHomClass F α β] : CoeTC F (sSupHom α β) :=
   ⟨fun f => ⟨f, map_sSup f⟩⟩