exists_basis_localizedModule_powers

English

If M is finitely presented and localized versions exist, a specified localized basis exists.

Русский

Если M конечно презентационный и существуют локализованные версии, существует базис локализации.

LaTeX

$$Module.FinitePresentation.exists_free_localizedModule_powers$$

Lean4

/-- If `M` is a finitely presented `R`-module,
then any `Rₛ`-basis of `Mₛ` for some `S : Submonoid R` can be lifted to
a `Rᵣ`-basis of `Mᵣ` for some `r ∈ S`.
-/
theorem exists_basis_localizedModule_powers (Rₛ) [CommRing Rₛ] [Algebra R Rₛ] [Module Rₛ M'] [IsScalarTower R Rₛ M']
    [IsLocalization S Rₛ] [Module.FinitePresentation R M] {I} [Finite I] (b : Basis I Rₛ M') :
    ∃ (r : R) (hr : r ∈ S) (b' : Basis I (Localization (.powers r)) (LocalizedModule (.powers r) M)),
      ∀ i,
        (LocalizedModule.lift (.powers r) f fun s ↦
              IsLocalizedModule.map_units f ⟨s.1, SetLike.le_def.mp (Submonoid.powers_le.mpr hr) s.2⟩)
            (b' i) =
          b i :=
  by
  have : Module.FinitePresentation R (I →₀ R) := Module.finitePresentation_of_projective _ _
  obtain ⟨r, hr, e, he⟩ :=
    Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule S f
      (Finsupp.mapRange.linearMap (Algebra.linearMap R Rₛ)) (b.repr.restrictScalars R)
  let e' :=
    IsLocalizedModule.iso (.powers r)
      (Finsupp.mapRange.linearMap (α := I) (Algebra.linearMap R (Localization (.powers r))))
  refine ⟨r, hr, .ofRepr (e ≪≫ₗ ?_), ?_⟩
  · exact { __ := e', toLinearMap := e'.extendScalarsOfIsLocalization (.powers r) (Localization (.powers r)) }
  · intro i
    have : e'.symm _ = _ :=
      LinearMap.congr_fun
        (IsLocalizedModule.iso_symm_comp (.powers r)
          (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (.powers r)))))
        (Finsupp.single i 1)
    simp only [Finsupp.mapRange.linearMap_apply, Finsupp.mapRange_single, Algebra.linearMap_apply, map_one,
      LocalizedModule.mkLinearMap_apply] at this
    change LocalizedModule.lift _ _ _ (e.symm (e'.symm _)) = _
    replace he := LinearMap.congr_fun he (e.symm (e'.symm (Finsupp.single i 1)))
    simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.apply_symm_apply, LinearEquiv.restrictScalars_apply] at he
    apply b.repr.injective
    rw [← he, Basis.repr_self, this, LocalizedModule.lift_mk]
    simp

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