Lemmas about IsBaseChange under exact sequences #
In this file, we show that for an R-algebra S taking cokernels commutes with base change
of modules from R to S.
If S is a flat R-algebra, the same holds for kernels,
see Mathlib.RingTheory.Flat.IsBaseChange.
Main Results #
For S an R-algebra, consider the following commutative diagram with exact rows,
M₁ M₂ M₃ R-modules, N₁ N₂ N₃ S-modules,
R-linear maps f₁ f₂ i₁ i₂ i₃ and S-linear maps g₁ g₂.
M₁ --f₁--> M₂ --f₂--> M₃ | | | i₁ i₂ i₃ | | | v v v N₁ --g₁--> N₂ --g₂--> N₃
IsBaseChange.of_right_exact: Iff₂andg₂are surjective,i₁andi₂is base change byS, theni₃is base change byS.
theorem
IsBaseChange.of_right_exact
{R : Type u_1}
[CommRing R]
(S : Type u_2)
[CommRing S]
[Algebra R S]
{M₁ : Type u_3}
{M₂ : Type u_4}
{M₃ : Type u_5}
{N₁ : Type u_6}
{N₂ : Type u_7}
{N₃ : Type u_8}
[AddCommGroup M₁]
[AddCommGroup M₂]
[AddCommGroup M₃]
[AddCommGroup N₁]
[AddCommGroup N₂]
[AddCommGroup N₃]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R N₁]
[Module R N₂]
[Module R N₃]
[Module S N₁]
[Module S N₂]
[Module S N₃]
[IsScalarTower R S N₁]
[IsScalarTower R S N₂]
[IsScalarTower R S N₃]
(h₁ : M₁ →ₗ[R] N₁)
(h₂ : M₂ →ₗ[R] N₂)
(h₃ : M₃ →ₗ[R] N₃)
{f : M₁ →ₗ[R] M₂}
{g : M₂ →ₗ[R] M₃}
{f' : N₁ →ₗ[S] N₂}
{g' : N₂ →ₗ[S] N₃}
(comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁)
(comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂)
(isb₁ : IsBaseChange S h₁)
(isb₂ : IsBaseChange S h₂)
(exact₁ : Function.Exact ⇑f ⇑g)
(surj₁ : Function.Surjective ⇑g)
(exact₂ : Function.Exact ⇑f' ⇑g')
(surj₂ : Function.Surjective ⇑g')
:
IsBaseChange S h₃