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₃