Kernel and cokernel equivalences for module localization

The actual localization functor preserves the two elementary constructions needed by the successor pages. The equivalences below are obtained from the canonical submodule and quotient localization equivalences in Mathlib.

noncomputable def AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedMap {R : Type u} [CommRing R] {U : Type v} {V : Type w} [AddCommGroup U] [AddCommGroup V] [Module R U] [Module R V] (S : Submonoid R) (f : U →ₗ[R] V) : LocalizedModule S U →ₗ[Localization S] LocalizedModule S V

The localization of an R-linear map, regarded as a map over the localized ring.

Equations

• AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedMap S f = LinearMap.extendScalarsOfIsLocalization S (Localization S) (↑R ((LocalizedModule.map S) f))

@[simp]

theorem AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedMap_apply {R : Type u} [CommRing R] {U : Type v} {V : Type w} [AddCommGroup U] [AddCommGroup V] [Module R U] [Module R V] (S : Submonoid R) (f : U →ₗ[R] V) (x : LocalizedModule S U) : (localizedMap S f) x = ((LocalizedModule.map S) f) x

noncomputable def AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedEquiv {R : Type u} [CommRing R] {U : Type v} {V : Type w} [AddCommGroup U] [AddCommGroup V] [Module R U] [Module R V] (S : Submonoid R) (e : U ≃ₗ[R] V) : LocalizedModule S U ≃ₗ[Localization S] LocalizedModule S V

Localization carries an actual linear equivalence to an equivalence over the localized ring.

Equations

• AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedEquiv S e = LinearEquiv.ofBijective (AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedMap S ↑e) ⋯

noncomputable def AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedKernelEquiv {R : Type u} [CommRing R] {U : Type v} {V : Type w} [AddCommGroup U] [AddCommGroup V] [Module R U] [Module R V] (S : Submonoid R) (f : U →ₗ[R] V) : LocalizedModule S ↥f.ker ≃ₗ[Localization S] ↥(localizedMap S f).ker

Localization commutes with kernels.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicAnalysis.LocalizedKernelCokernelEquivalences.localizedCokernelEquiv {R : Type u} [CommRing R] {U : Type v} {V : Type w} [AddCommGroup U] [AddCommGroup V] [Module R U] [Module R V] (S : Submonoid R) (f : U →ₗ[R] V) : LocalizedModule S (V ⧸ f.range) ≃ₗ[Localization S] LocalizedModule S V ⧸ (localizedMap S f).range

Localization commutes with cokernels.

Equations

• One or more equations did not get rendered due to their size.