Theorems · Theorem · commutative algebra

IsBaseChange.of_left_exact

∀ {R : Type u_1} [inst : CommRing R] (S : Type u_2) [inst_1 : CommRing S] [inst_2 : 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} [inst_3 : AddCommGroup M₁]
  [inst_4 : AddCommGroup M₂] [inst_5 : AddCommGroup M₃] [inst_6 : AddCommGroup N₁] [inst_7 : AddCommGroup N₂]
  [inst_8 : AddCommGroup N₃] [inst_9 : Module R M₁] [inst_10 : Module R M₂] [inst_11 : Module R M₃]
  [inst_12 : Module R N₁] [inst_13 : Module R N₂] [inst_14 : Module R N₃] [inst_15 : Module S N₁]
  [inst_16 : Module S N₂] [inst_17 : Module S N₃] [inst_18 : IsScalarTower R S N₁] [inst_19 : IsScalarTower R S N₂]
  [inst_20 : 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₃},
  h₂ ∘ₗ f = ↑R f' ∘ₗ h₁ →
    h₃ ∘ₗ g = ↑R g' ∘ₗ h₂ →
      ∀ [Module.Flat R S],
        IsBaseChange S h₂ →
          IsBaseChange S h₃ →
            Function.Exact ⇑f ⇑g →
              Function.Injective ⇑f → Function.Exact ⇑f' ⇑g' → Function.Injective ⇑f' → IsBaseChange S h₁

Defined in

Mathlib.RingTheory.Flat.IsBaseChange

Cited by

1 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAddCommGroupAddCommGroupAddCommGroupAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleModuleModuleModuleModuleModuleModuleIsScalarTowerIsScalarTowerIsScalarTowerModule.Flat