ArtinianSecondaryAnnihilator.lean

theorem surjective_pow_smul_of_surjective_smul
    (r : R) (hr : Function.Surjective (fun z : M => r • z)) (n : ℕ) :
    Function.Surjective (fun z : M => r ^ n • z) := by
  induction n with
  | zero =>
      intro z
      exact ⟨z, by simp only [pow_zero, one_smul]⟩
  | succ n ih =>
      intro z
      obtain ⟨w, hw⟩ := hr z
      obtain ⟨v, hv⟩ := ih w
      exact ⟨v, by simpa only [pow_succ', mul_smul, hv] using hw⟩

theorem IsSecondaryModule.surjective_smul_iff
    (hM : IsSecondaryModule R M) (r : R) :
    Function.Surjective (fun z : M => r • z) ↔
      r ∉ (Module.annihilator R M).radical := by
  let : Nontrivial M := hM.1
  constructor
  · intro hr hmem
    obtain ⟨n, hn⟩ := hmem
    obtain ⟨z, hz⟩ := exists_ne (0 : M)
    obtain ⟨w, hw⟩ := surjective_pow_smul_of_surjective_smul r hr n z
    exact hz (hw.symm.trans (Module.mem_annihilator.mp hn w))
  · intro hr
    rcases hM.2 r with hsurj | ⟨n, hn⟩
    · exact hsurj
    · exact False.elim (hr ⟨n, Module.mem_annihilator.mpr hn⟩)

theorem IsSecondaryModule.radical_annihilator_isPrime
    (hM : IsSecondaryModule R M) :
    (Module.annihilator R M).radical.IsPrime