Algebra homomorphisms and ideals under pushout

Let S' be the pushout of R → S along R → R', as expressed by Algebra.IsPushout R S R' S'. Mathlib's Algebra.pushoutDesc describes the R-algebra homomorphisms out of S'. This file describes the R'-algebra homomorphisms out of S': they are determined by their restrictions to S, and every R-algebra homomorphism out of S extends to one. It also describes the ring homomorphisms out of S', into a ring carrying no algebra structure: they are determined by their restrictions to S and R', and every pair of ring homomorphisms out of S and R' which agree on R glues to one. It also records the naturality of Algebra.IsPushout.cancelBaseChangeAlg in the coefficient algebra.

For an ideal of R', its extension to the pushout S' is spanned over S by its image. This identifies extension of ideals with extension of the underlying submodule.

Main definitions

• Algebra.IsPushout.lift f: the R'-algebra homomorphism S' →ₐ[R'] A extending an R-algebra homomorphism f : S →ₐ[R] A along S → S'.
• Algebra.IsPushout.liftRingHom x y h: the ring homomorphism S' →+* T restricting to ring homomorphisms x : S →+* T and y : R' →+* T which agree on R.

Main results

• Algebra.IsPushout.lift_algebraMap: lift f restricts to f on S.
• Algebra.IsPushout.algHom_ext': R'-algebra homomorphisms out of S' agreeing on S are equal.
• Algebra.IsPushout.ringHom_ext: ring homomorphisms out of S' agreeing on S and on R' are equal.
• Ideal.restrictScalars_map_eq_span: the extension to S' of an ideal J of R' is the S-span of the image of J.
• Module.Finite.of_isPushout, Module.Projective.of_isPushout, Algebra.FinitePresentation.of_isPushout: finiteness, projectivity and finite presentation are stable under pushout.
• Algebra.IsPushout.adjoin_image_eq_top: generators of S over R map to generators of S' over R'; Algebra.IsPushout.adjoin_zero_union_one_eq_top is the case of generation in degrees 0 and 1 along a graded ring homomorphism.
• Algebra.IsPushout.cancelBaseChangeAlg_symm_lTensor: the isomorphism S ⊗[R] T ≃ₐ[S] S' ⊗[R'] T is natural in the R'-algebra T.

noncomputable def Algebra.IsPushout.lift {R : Type u_1} {S : Type u_2} (R' : Type u_3) {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {A : Type u_5} [Semiring A] [Algebra R' A] [Algebra R A] [IsScalarTower R R' A] (f : S →ₐ[R] A) : S' →ₐ[R'] A

The R'-algebra homomorphism out of the pushout S' extending an R-algebra homomorphism f : S →ₐ[R] A along S → S'.

@[simp]

theorem Algebra.IsPushout.lift_algebraMap {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {A : Type u_5} [Semiring A] [Algebra R' A] [Algebra R A] [IsScalarTower R R' A] (f : S →ₐ[R] A) (s : S) : (lift R' f) ((algebraMap S S') s) = f s

lift R' f restricts to f on S.

theorem Algebra.IsPushout.algHom_ext' {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {A : Type u_5} [Semiring A] [Algebra R' A] [Algebra R A] [IsScalarTower R R' A] {f g : S' →ₐ[R'] A} : (AlgHom.restrictScalars R f).comp (IsScalarTower.toAlgHom R S S') = (AlgHom.restrictScalars R g).comp (IsScalarTower.toAlgHom R S S') → f = g

Two R'-algebra homomorphisms out of the pushout S' that agree on S are equal.

theorem Algebra.IsPushout.ringHom_ext {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {T : Type u_5} [Semiring T] {f g : S' →+* T} (hS : f.comp (algebraMap S S') = g.comp (algebraMap S S')) (hR' : f.comp (algebraMap R' S') = g.comp (algebraMap R' S')) : f = g

Two ring homomorphisms out of the pushout S' that agree on S and on R' are equal.

noncomputable def Algebra.IsPushout.liftRingHom {R : Type u_1} {S : Type u_2} {R' : Type u_3} (S' : Type u_4) [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {T : Type u_5} [CommSemiring T] (x : S →+* T) (y : R' →+* T) (hxy : x.comp (algebraMap R S) = y.comp (algebraMap R R')) : S' →+* T

The ring homomorphism out of the pushout S' = S ⊗[R] R' restricting to ring homomorphisms x : S →+* T and y : R' →+* T which agree on R. No algebra structure on T is involved.

@[simp]

theorem Algebra.IsPushout.liftRingHom_algebraMap_left {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {T : Type u_5} [CommSemiring T] (x : S →+* T) (y : R' →+* T) (hxy : x.comp (algebraMap R S) = y.comp (algebraMap R R')) (s : S) : (liftRingHom S' x y hxy) ((algebraMap S S') s) = x s

liftRingHom S' x y hxy restricts to x on S.

@[simp]

theorem Algebra.IsPushout.liftRingHom_algebraMap_right {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {T : Type u_5} [CommSemiring T] (x : S →+* T) (y : R' →+* T) (hxy : x.comp (algebraMap R S) = y.comp (algebraMap R R')) (r : R') : (liftRingHom S' x y hxy) ((algebraMap R' S') r) = y r

liftRingHom S' x y hxy restricts to y on R'.

theorem Ideal.restrictScalars_map_eq_span {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : Algebra.IsPushout R S R' S'] (J : Ideal R') : Submodule.restrictScalars S (map (algebraMap R' S') J) = Submodule.span S (⇑(algebraMap R' S') '' ↑J)

In a pushout S' = S ⊗[R] R', the extension of an ideal J of R' is spanned over S by the image of J.

theorem Module.Finite.of_isPushout (R : Type u_1) (S : Type u_2) (R' : Type u_3) (S' : Type u_4) [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : Algebra.IsPushout R S R' S'] [Module.Finite R S] : Module.Finite R' S'

Finiteness as a module is stable under pushout: if S is a finite R-module, then the pushout S' is a finite R'-module.

theorem Module.Projective.of_isPushout (R : Type u_1) (S : Type u_2) (R' : Type u_3) (S' : Type u_4) [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : Algebra.IsPushout R S R' S'] [Projective R S] : Projective R' S'

Projectivity as a module is stable under pushout: if S is a projective R-module, then the pushout S' is a projective R'-module.

theorem Algebra.IsPushout.adjoin_image_eq_top {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {s : Set S} (hs : adjoin R s = ⊤) : adjoin R' (⇑(algebraMap S S') '' s) = ⊤

Generators pass to the pushout: if s generates S as an R-algebra, then its image generates the pushout S' as an R'-algebra.

theorem Algebra.IsPushout.adjoin_zero_union_one_eq_top {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommSemiring R] [CommSemiring S] [CommSemiring R'] [CommSemiring S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [h : IsPushout R S R' S'] {σ : Type u_5} {τ : Type u_6} [SetLike σ S] [SetLike τ S'] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} (φ : 𝒜 →+*ᵍ ℬ) (hφ : ∀ (x : S), φ x = (algebraMap S S') x) (hs : adjoin R (↑(𝒜 0) ∪ ↑(𝒜 1)) = ⊤) : adjoin R' (↑(ℬ 0) ∪ ↑(ℬ 1)) = ⊤

Generation in degrees 0 and 1 passes to the pushout along a graded ring homomorphism: if S is generated over R by its homogeneous elements of degrees 0 and 1, and S → S' underlies a graded ring homomorphism, then S' is generated over R' by its homogeneous elements of degrees 0 and 1.

theorem Algebra.FinitePresentation.of_isPushout (R : Type u_1) (S : Type u_2) (R' : Type u_3) (S' : Type u_4) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] [FinitePresentation R S] : FinitePresentation R' S'

Finite presentation is stable under pushout: if S is a finitely presented R-algebra, then the pushout S' is a finitely presented R'-algebra.

theorem Algebra.IsPushout.cancelBaseChangeAlg_symm_lTensor {R : Type u_1} {S : Type u_2} {R' : Type u_3} (S' : Type u_4) [CommSemiring R] [CommSemiring S] [CommRing R'] [CommRing S'] [Algebra R S] [Algebra R R'] [Algebra R' S'] [Algebra R S'] [Algebra S S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] [IsPushout R S R' S'] {T : Type u_5} {T' : Type u_6} [CommRing T] [Algebra R' T] [Algebra R T] [IsScalarTower R R' T] [CommRing T'] [Algebra R' T'] [Algebra R T'] [IsScalarTower R R' T'] (g : T →ₐ[R'] T') (z : TensorProduct R S T) : (cancelBaseChangeAlg R S R' S' T').symm ((TensorProduct.lTensor S (AlgHom.restrictScalars R g)) z) = (TensorProduct.lTensor S' g) ((cancelBaseChangeAlg R S R' S' T).symm z)

The isomorphism S ⊗[R] T ≃ₐ[S] S' ⊗[R'] T is natural in the R'-algebra T.