English
The pushout descent evaluated on the right-hand leg equals the right map g on S'.
Русский
pushoutDesc на правой ножке даёт g на S'.
LaTeX
$$Algebra.pushoutDesc_right S' f g H (algebraMap R' S' x) = g x$$
Lean4
/-- 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'`.
-/
theorem comp_iff {T' : Type*} [CommSemiring T'] [Algebra R T'] [Algebra S' T'] [Algebra S T'] [Algebra T T']
[Algebra R' T'] [IsScalarTower R T T'] [IsScalarTower S T T'] [IsScalarTower S S' T'] [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' :=
by
let f : R' →ₗ[R] S' := (IsScalarTower.toAlgHom R R' S').toLinearMap
haveI : IsScalarTower R S T' :=
.of_algebraMap_eq fun x ↦ by rw [algebraMap_apply R S' T', algebraMap_apply R S S', ← algebraMap_apply S S' T']
have heq : (toAlgHom S S' T').toLinearMap.restrictScalars R ∘ₗ f = (toAlgHom R R' T').toLinearMap :=
by
ext x
simp [f, ← IsScalarTower.algebraMap_apply]
rw [isPushout_iff, isPushout_iff, ← heq, IsBaseChange.comp_iff]
exact Algebra.IsPushout.out
