map_exact — Mathlib

English

AdicCompletion preserves exactness for a Noetherian ring and finite modules: if f,g are short exact in M,N,P, then map I f, map I g form a short exact sequence as well.

Русский

Адическое завершение сохраняет точность для нетеровской кольца и конечных модулей: отображения map I f, map I g образуют точную последовательность.

LaTeX

$$$\text{Function.Exact}(\mathrm{map}\ I\ f,\ \mathrm{map}\ I\ g)$$$

Lean4

/-- `AdicCompletion` over a Noetherian ring is exact on finitely generated modules. -/
theorem map_exact : Function.Exact (map I f) (map I g) :=
  by
  refine LinearMap.exact_of_comp_eq_zero_of_ker_le_range ?_ (fun y ↦ ?_)
  · rw [map_comp, hfg.linearMap_comp_eq_zero, AdicCompletion.map_zero]
  · apply AdicCompletion.induction_on I N y (fun b ↦ ?_)
    intro hz
    obtain ⟨k, hk⟩ := Ideal.exists_pow_inf_eq_pow_smul I (LinearMap.range f)
    have hb (n : ℕ) : g (b n) ∈ (I ^ n • ⊤ : Submodule R P) := by simpa using congrArg (fun x ↦ x.val n) hz
    let a := mapExactAux hf hfg hg hk b hb
    refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
    · refine fun n ↦ SModEq.symm ?_
      simp [a, mapExactAux, SModEq]
    · ext n
      suffices h :
        Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (f (a n)) =
          Submodule.Quotient.mk (p := (I ^ n • ⊤ : Submodule R N)) (b (k + n))
        by simp [h, AdicCauchySequence.mk_eq_mk (show n ≤ k + n by cutsat)]
      rw [Submodule.Quotient.eq]
      have hle : (I ^ (k + n) • ⊤ : Submodule R N) ≤ (I ^ n • ⊤ : Submodule R N) :=
        Submodule.smul_mono_left (Ideal.pow_le_pow_right (by cutsat))
      exact hle (a n).property

Похожие утверждения