split_surjective_of_localization_maximal

English

If a linear map splits after localization at maximal ideals, then there is a global splitting over the base ring.

Русский

Если линейное отображение распадается после локализации по максимальным идеалам, существует глобальное расщепление над базовым кольцом.

LaTeX

$$$\\exists g: N \\to M,\\; f \\circ g = \\mathrm{id}_N$ proven after localization implies existence of global g with f \\circ g = id.$$

Lean4

theorem split_surjective_of_localization_maximal (f : M →ₗ[R] N) [Module.FinitePresentation R N]
    (H :
      ∀ (I : Ideal R) (_ : I.IsMaximal),
        ∃ (g : _ →ₗ[Localization.AtPrime I] _), (LocalizedModule.map I.primeCompl f).comp g = LinearMap.id) :
    ∃ (g : N →ₗ[R] M), f.comp g = LinearMap.id :=
  by
  change LinearMap.id ∈ LinearMap.range (LinearMap.llcomp R N M N f)
  refine Submodule.mem_of_localization_maximal _ (fun P _ ↦ LocalizedModule.map P.primeCompl) _ _ fun I hI ↦ ?_
  rw [LocalizedModule.map_id]
  have :
    LinearMap.id ∈
      LinearMap.range (LinearMap.llcomp _ (LocalizedModule I.primeCompl N) _ _ (LocalizedModule.map I.primeCompl f)) :=
    H I hI
  convert this
  · ext f
    constructor
    · intro hf
      obtain ⟨a, ha, c, rfl⟩ := hf
      obtain ⟨g, rfl⟩ := ha
      use IsLocalizedModule.mk' (LocalizedModule.map I.primeCompl) g c
      apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units (LocalizedModule.map I.primeCompl) c).injective
      dsimp
      conv_rhs => rw [← Submonoid.smul_def]
      conv_lhs => rw [← LinearMap.map_smul_of_tower]
      rw [← Submonoid.smul_def, IsLocalizedModule.mk'_cancel', IsLocalizedModule.mk'_cancel']
      apply LinearMap.restrictScalars_injective R
      apply IsLocalizedModule.ext I.primeCompl (LocalizedModule.mkLinearMap I.primeCompl N)
      · exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)
      ext
      simp only [LocalizedModule.map_mk, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
        LocalizedModule.mkLinearMap_apply, LinearMap.llcomp_apply, LocalizedModule.map_mk]
    · rintro ⟨g, rfl⟩
      obtain ⟨⟨g, s⟩, rfl⟩ := IsLocalizedModule.mk'_surjective I.primeCompl (LocalizedModule.map I.primeCompl) g
      simp only [Function.uncurry_apply_pair]
      refine ⟨f.comp g, ⟨g, rfl⟩, s, ?_⟩
      apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units (LocalizedModule.map I.primeCompl) s).injective
      simp only [Module.algebraMap_end_apply, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel',
        ← LinearMap.map_smul_of_tower]
      apply LinearMap.restrictScalars_injective R
      apply IsLocalizedModule.ext I.primeCompl (LocalizedModule.mkLinearMap I.primeCompl N)
      · exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)
      ext
      simp only [coe_comp, coe_restrictScalars, Function.comp_apply, LocalizedModule.mkLinearMap_apply,
        LocalizedModule.map_mk, llcomp_apply]

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