Localization of modules is an exact functor #
Main definitions #
LocalizedModule.map_exact: Localization of modules is an exact functor.IsLocalizedModule.map_exact: A variant expressed in terms ofIsLocalizedModule.
theorem
LocalizedModule.map_exact
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
{M₀ : Type u_2}
[AddCommMonoid M₀]
[Module R M₀]
{M₁ : Type u_3}
[AddCommMonoid M₁]
[Module R M₁]
{M₂ : Type u_4}
[AddCommMonoid M₂]
[Module R M₂]
(g : M₀ →ₗ[R] M₁)
(h : M₁ →ₗ[R] M₂)
(ex : Function.Exact ⇑g ⇑h)
:
Function.Exact ⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₀) (LocalizedModule.mkLinearMap S M₁)) g)
⇑((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M₁) (LocalizedModule.mkLinearMap S M₂)) h)
Localization of modules is an exact functor, proven here for LocalizedModule.
See IsLocalizedModule.map_exact for the more general version.
theorem
IsLocalizedModule.map_exact
{R : Type u_1}
[CommSemiring R]
(S : Submonoid R)
{M₀ : Type u_2}
{M₀' : Type u_5}
[AddCommMonoid M₀]
[AddCommMonoid M₀']
[Module R M₀]
[Module R M₀']
(f₀ : M₀ →ₗ[R] M₀')
[IsLocalizedModule S f₀]
{M₁ : Type u_3}
{M₁' : Type u_6}
[AddCommMonoid M₁]
[AddCommMonoid M₁']
[Module R M₁]
[Module R M₁']
(f₁ : M₁ →ₗ[R] M₁')
[IsLocalizedModule S f₁]
{M₂ : Type u_4}
{M₂' : Type u_7}
[AddCommMonoid M₂]
[AddCommMonoid M₂']
[Module R M₂]
[Module R M₂']
(f₂ : M₂ →ₗ[R] M₂')
[IsLocalizedModule S f₂]
(g : M₀ →ₗ[R] M₁)
(h : M₁ →ₗ[R] M₂)
(ex : Function.Exact ⇑g ⇑h)
:
Function.Exact ⇑((IsLocalizedModule.map S f₀ f₁) g) ⇑((IsLocalizedModule.map S f₁ f₂) h)
Localization of modules is an exact functor.