Theorems · Theorem · commutative algebra

Algebra.IsPushout.comp_iff

∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {T : Type u_4}
  [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (R' : Type u_6)
  (S' : Type u_7) [inst_7 : CommSemiring R'] [inst_8 : CommSemiring S'] [inst_9 : Algebra R R'] [inst_10 : Algebra S S']
  [inst_11 : Algebra R' S'] [inst_12 : Algebra R S'] [inst_13 : IsScalarTower R R' S'] [inst_14 : IsScalarTower R S S']
  {T' : Type u_8} [inst_15 : CommSemiring T'] [inst_16 : Algebra R T'] [inst_17 : Algebra S' T']
  [inst_18 : Algebra S T'] [inst_19 : Algebra T T'] [inst_20 : Algebra R' T'] [inst_21 : IsScalarTower R T T']
  [inst_22 : IsScalarTower S T T'] [inst_23 : IsScalarTower S S' T'] [inst_24 : IsScalarTower R R' T']
  [IsScalarTower R S' T'] [IsScalarTower R' S' T'] [Algebra.IsPushout R S R' S'],
  Algebra.IsPushout R T R' T' ↔ Algebra.IsPushout S T S' T'

Let the following be a commutative diagram of rings `` R → S → T ↓ ↓ ↓ R' → S' → T' ` where the left-hand square is a pushout. Then the following are equivalent: - the big rectangle is a pushout. - the right-hand square is a pushout. Note that this is essentially the isomorphism T ⊗[S] (S ⊗[R] R') ≃ₐ[T] T ⊗[R] R'`.

Defined in

Mathlib.RingTheory.IsTensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraAlgebraIsScalarTowerCommSemiringCommSemiringAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerCommSemiringAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTowerIsScalarTowerAlgebra.IsPushout