English
If there exists a nonzero finitely generated R-submodule N of M invariant under the action of x ∈ A, then x is integral over R.
Русский
Если существует ненулевой FG-R-подмодуль N подмодуля M, сохраняемый действием x ∈ A, то x интегральный над R.
LaTeX
$$$\exists N \le M:\ N \neq \{0\},\; N \text{ FG as }R\text{-module},\; \forall n\in N:\ x\cdot n \in N \Rightarrow IsIntegral(R, x).$$$
Lean4
/-- Suppose `A` is an `R`-algebra, `M` is an `A`-module such that `a • m ≠ 0` for all non-zero `a`
and `m`. If `x : A` fixes a nontrivial f.g. `R`-submodule `N` of `M`, then `x` is `R`-integral. -/
theorem isIntegral_of_smul_mem_submodule {M : Type*} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
[NoZeroSMulDivisors A M] (N : Submodule R M) (hN : N ≠ ⊥) (hN' : N.FG) (x : A) (hx : ∀ n ∈ N, x • n ∈ N) :
IsIntegral R x :=
by
let A' : Subalgebra R A :=
{ carrier := {x | ∀ n ∈ N, x • n ∈ N}
mul_mem' := fun {a b} ha hb n hn => smul_smul a b n ▸ ha _ (hb _ hn)
one_mem' := fun n hn => (one_smul A n).symm ▸ hn
add_mem' := fun {a b} ha hb n hn => (add_smul a b n).symm ▸ N.add_mem (ha _ hn) (hb _ hn)
zero_mem' := fun n _hn => (zero_smul A n).symm ▸ N.zero_mem
algebraMap_mem' := fun r n hn => (algebraMap_smul A r n).symm ▸ N.smul_mem r hn }
let f : A' →ₐ[R] Module.End R N :=
AlgHom.ofLinearMap
{ toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict x.prop
map_add' := by intro x y; ext; exact add_smul _ _ _
map_smul' := by intro r s; ext; apply smul_assoc } (by ext; apply one_smul) (by intro x y; ext; apply mul_smul)
obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ N, a ≠ (0 : M) := by
by_contra! h'
apply hN
rwa [eq_bot_iff]
have : Function.Injective f := by
change Function.Injective f.toLinearMap
rw [← LinearMap.ker_eq_bot, eq_bot_iff]
intro s hs
have : s.1 • a = 0 := congr_arg Subtype.val (LinearMap.congr_fun hs ⟨a, ha₁⟩)
exact Subtype.ext ((eq_zero_or_eq_zero_of_smul_eq_zero this).resolve_right ha₂)
change IsIntegral R (A'.val ⟨x, hx⟩)
rw [isIntegral_algHom_iff A'.val Subtype.val_injective, ← isIntegral_algHom_iff f this]
haveI : Module.Finite R N := by rwa [Module.finite_def, Submodule.fg_top]
apply Algebra.IsIntegral.isIntegral
