The characteristice predicate of tensor product #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
is_tensor_product: A predicate onf : M₁ →ₗ[R] M₂ →ₗ[R] Mexpressing thatfrealizesMas the tensor product ofM₁ ⊗[R] M₂. This is defined by requiring the liftM₁ ⊗[R] M₂ → Mto be bijective.is_base_change: A predicate on anR-algebraSand a mapf : M →ₗ[R] NwithNbeing aS-module, expressing thatfrealizesNas the base change ofMalongR → S.algebra.is_pushout: A predicate on the following diagram of scalar towersasserting that is a pushout diagram (i.e.R → S ↓ ↓ R' → S'S' = S ⊗[R] R')
Main results #
tensor_product.is_base_change:S ⊗[R] Mis the base change ofMalongR → S.
def
is_tensor_product
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
(f : M₁ →ₗ[R] M₂ →ₗ[R] M) :
Prop
Given a bilinear map f : M₁ →ₗ[R] M₂ →ₗ[R] M, is_tensor_product f means that
M is the tensor product of M₁ and M₂ via f.
This is defined by requiring the lift M₁ ⊗[R] M₂ → M to be bijective.
Equations
theorem
tensor_product.is_tensor_product
(R : Type u_1)
[comm_ring R]
(M : Type u_4)
[add_comm_monoid M]
[module R M]
(N : Type u_8)
[add_comm_monoid N]
[module R N] :
is_tensor_product (tensor_product.mk R M N)
noncomputable
def
is_tensor_product.equiv
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
(h : is_tensor_product f) :
tensor_product R M₁ M₂ ≃ₗ[R] M
If M is the tensor product of M₁ and M₂, it is linearly equivalent to M₁ ⊗[R] M₂.
Equations
@[simp]
theorem
is_tensor_product.equiv_apply
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
(h : is_tensor_product f)
(ᾰ : tensor_product R M₁ M₂) :
⇑(h.equiv) ᾰ = ⇑(tensor_product.lift f) ᾰ
@[simp]
theorem
is_tensor_product.equiv_to_linear_map
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
(h : is_tensor_product f) :
@[simp]
theorem
is_tensor_product.equiv_symm_apply
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
(h : is_tensor_product f)
(x₁ : M₁)
(x₂ : M₂) :
noncomputable
def
is_tensor_product.lift
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
{M' : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[add_comm_monoid M']
[module R M₁]
[module R M₂]
[module R M]
[module R M']
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
(h : is_tensor_product f)
(f' : M₁ →ₗ[R] M₂ →ₗ[R] M') :
If M is the tensor product of M₁ and M₂, we may lift a bilinear map M₁ →ₗ[R] M₂ →ₗ[R] M'
to a M →ₗ[R] M'.
Equations
- h.lift f' = (tensor_product.lift f').comp h.equiv.symm.to_linear_map
theorem
is_tensor_product.lift_eq
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
{M' : Type u_5}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[add_comm_monoid M']
[module R M₁]
[module R M₂]
[module R M]
[module R M']
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
(h : is_tensor_product f)
(f' : M₁ →ₗ[R] M₂ →ₗ[R] M')
(x₁ : M₁)
(x₂ : M₂) :
noncomputable
def
is_tensor_product.map
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
{N₁ : Type u_6}
{N₂ : Type u_7}
{N : Type u_8}
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[add_comm_monoid N]
[module R N₁]
[module R N₂]
[module R N]
{g : N₁ →ₗ[R] N₂ →ₗ[R] N}
(hf : is_tensor_product f)
(hg : is_tensor_product g)
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂) :
The tensor product of a pair of linear maps between modules.
Equations
- hf.map hg i₁ i₂ = hg.equiv.to_linear_map.comp ((tensor_product.map i₁ i₂).comp hf.equiv.symm.to_linear_map)
theorem
is_tensor_product.map_eq
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
{N₁ : Type u_6}
{N₂ : Type u_7}
{N : Type u_8}
[add_comm_monoid N₁]
[add_comm_monoid N₂]
[add_comm_monoid N]
[module R N₁]
[module R N₂]
[module R N]
{g : N₁ →ₗ[R] N₂ →ₗ[R] N}
(hf : is_tensor_product f)
(hg : is_tensor_product g)
(i₁ : M₁ →ₗ[R] N₁)
(i₂ : M₂ →ₗ[R] N₂)
(x₁ : M₁)
(x₂ : M₂) :
theorem
is_tensor_product.induction_on
{R : Type u_1}
[comm_ring R]
{M₁ : Type u_2}
{M₂ : Type u_3}
{M : Type u_4}
[add_comm_monoid M₁]
[add_comm_monoid M₂]
[add_comm_monoid M]
[module R M₁]
[module R M₂]
[module R M]
{f : M₁ →ₗ[R] M₂ →ₗ[R] M}
(h : is_tensor_product f)
{C : M → Prop}
(m : M)
(h0 : C 0)
(htmul : ∀ (x : M₁) (y : M₂), C (⇑(⇑f x) y))
(hadd : ∀ (x y : M), C x → C y → C (x + y)) :
C m
def
is_base_change
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
(S : Type v₃)
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
(f : M →ₗ[R] N) :
Prop
Given an R-algebra S and an R-module M, an S-module N together with a map
f : M →ₗ[R] N is the base change of M to S if the map S × M → N, (s, m) ↦ s • f m is the
tensor product.
Equations
- is_base_change S f = is_tensor_product (linear_map.restrict_scalars R (⇑((algebra.of_id S (module.End S (M →ₗ[R] N))).to_linear_map.flip) f))
noncomputable
def
is_base_change.lift
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
{Q : Type u_3}
[add_comm_monoid Q]
[module S Q]
[module R Q]
[is_scalar_tower R S Q]
(g : M →ₗ[R] Q) :
Suppose f : M →ₗ[R] N is the base change of M along R → S. Then any R-linear map from
M to an S-module factors thorugh f.
Equations
- h.lift g = {to_fun := (is_tensor_product.lift h (linear_map.restrict_scalars R (⇑((algebra.of_id S (module.End S (M →ₗ[R] Q))).to_linear_map.flip) g))).to_fun, map_add' := _, map_smul' := _}
theorem
is_base_change.lift_eq
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
{Q : Type u_3}
[add_comm_monoid Q]
[module S Q]
[module R Q]
[is_scalar_tower R S Q]
(g : M →ₗ[R] Q)
(x : M) :
theorem
is_base_change.lift_comp
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
{Q : Type u_3}
[add_comm_monoid Q]
[module S Q]
[module R Q]
[is_scalar_tower R S Q]
(g : M →ₗ[R] Q) :
(linear_map.restrict_scalars R (h.lift g)).comp f = g
theorem
is_base_change.induction_on
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
(x : N)
(P : N → Prop)
(h₁ : P 0)
(h₂ : ∀ (m : M), P (⇑f m))
(h₃ : ∀ (s : S) (n : N), P n → P (s • n))
(h₄ : ∀ (n₁ n₂ : N), P n₁ → P n₂ → P (n₁ + n₂)) :
P x
theorem
is_base_change.alg_hom_ext
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
{Q : Type u_3}
[add_comm_monoid Q]
[module S Q]
(g₁ g₂ : N →ₗ[S] Q)
(e : ∀ (x : M), ⇑g₁ (⇑f x) = ⇑g₂ (⇑f x)) :
g₁ = g₂
theorem
is_base_change.alg_hom_ext'
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
{Q : Type u_3}
[add_comm_monoid Q]
[module S Q]
[module R Q]
[is_scalar_tower R S Q]
(g₁ g₂ : N →ₗ[S] Q)
(e : (linear_map.restrict_scalars R g₁).comp f = (linear_map.restrict_scalars R g₂).comp f) :
g₁ = g₂
theorem
tensor_product.is_base_change
(R : Type u_1)
(M : Type v₁)
(S : Type v₃)
[add_comm_monoid M]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M] :
is_base_change S (⇑(tensor_product.mk R S M) 1)
noncomputable
def
is_base_change.equiv
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f) :
tensor_product R S M ≃ₗ[S] N
The base change of M along R → S is linearly equivalent to S ⊗[R] M.
theorem
is_base_change.equiv_tmul
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
(s : S)
(m : M) :
theorem
is_base_change.equiv_symm_apply
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N}
(h : is_base_change S f)
(m : M) :
theorem
is_base_change.of_lift_unique
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
(f : M →ₗ[R] N)
(h : ∀ (Q : Type (max v₁ v₂ v₃)) [_inst_14 : add_comm_monoid Q] [_inst_15 : module R Q] [_inst_16 : module S Q] [_inst_15_1 : is_scalar_tower R S Q] (g : M →ₗ[R] Q), ∃! (g' : N →ₗ[S] Q), (linear_map.restrict_scalars R g').comp f = g) :
is_base_change S f
theorem
is_base_change.iff_lift_unique
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{f : M →ₗ[R] N} :
is_base_change S f ↔ ∀ (Q : Type (max v₁ v₂ v₃)) [_inst_14 : add_comm_monoid Q] [_inst_15 : module R Q] [_inst_16 : module S Q] [_inst_15_1 : is_scalar_tower R S Q] (g : M →ₗ[R] Q), ∃! (g' : N →ₗ[S] Q), (linear_map.restrict_scalars R g').comp f = g
theorem
is_base_change.of_equiv
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[module R M]
[module R N]
(e : M ≃ₗ[R] N) :
theorem
is_base_change.comp
{R : Type u_1}
{M : Type v₁}
{N : Type v₂}
{S : Type v₃}
[add_comm_monoid M]
[add_comm_monoid N]
[comm_ring R]
[comm_ring S]
[algebra R S]
[module R M]
[module R N]
[module S N]
[is_scalar_tower R S N]
{T : Type u_4}
{O : Type u_5}
[comm_ring T]
[algebra R T]
[algebra S T]
[is_scalar_tower R S T]
[add_comm_monoid O]
[module R O]
[module S O]
[module T O]
[is_scalar_tower S T O]
[is_scalar_tower R S O]
[is_scalar_tower R T O]
{f : M →ₗ[R] N}
(hf : is_base_change S f)
{g : N →ₗ[S] O}
(hg : is_base_change T g) :
is_base_change T ((linear_map.restrict_scalars R g).comp f)
@[class]
structure
algebra.is_pushout
(R : Type u_1)
(S : Type v₃)
[comm_ring R]
[comm_ring S]
[algebra R S]
(R' : Type u_6)
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S'] :
Prop
- out : is_base_change S (is_scalar_tower.to_alg_hom R R' S').to_linear_map
A type-class stating that the following diagram of scalar towers
R → S
↓ ↓
R' → S'
is a pushout diagram (i.e. S' = S ⊗[R] R')
Instances of this typeclass
theorem
algebra.is_pushout_iff
(R : Type u_1)
(S : Type v₃)
[comm_ring R]
[comm_ring S]
[algebra R S]
(R' : Type u_6)
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S'] :
algebra.is_pushout R S R' S' ↔ is_base_change S (is_scalar_tower.to_alg_hom R R' S').to_linear_map
theorem
algebra.is_pushout.symm
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
{S' : Type u_7}
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
(h : algebra.is_pushout R S R' S') :
algebra.is_pushout R R' S S'
theorem
algebra.is_pushout.comm
(R : Type u_1)
(S : Type v₃)
[comm_ring R]
[comm_ring S]
[algebra R S]
(R' : Type u_6)
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S'] :
algebra.is_pushout R S R' S' ↔ algebra.is_pushout R R' S S'
@[protected, instance]
def
tensor_product.is_pushout
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra R T] :
algebra.is_pushout R S T (tensor_product R S T)
@[protected, instance]
def
tensor_product.is_pushout'
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra R T] :
algebra.is_pushout R T S (tensor_product R S T)
theorem
algebra.pushout_desc_apply
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
[H : algebra.is_pushout R S R' S']
{A : Type u_2}
[semiring A]
[algebra R A]
(f : S →ₐ[R] A)
(g : R' →ₐ[R] A)
(hf : ∀ (x : S) (y : R'), ⇑f x * ⇑g y = ⇑g y * ⇑f x)
(ᾰ : S') :
⇑(algebra.pushout_desc S' f g hf) ᾰ = ⇑(algebra.is_pushout.out.lift g.to_linear_map) ᾰ
noncomputable
def
algebra.pushout_desc
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
[H : algebra.is_pushout R S R' S']
{A : Type u_2}
[semiring A]
[algebra R A]
(f : S →ₐ[R] A)
(g : R' →ₐ[R] A)
(hf : ∀ (x : S) (y : R'), ⇑f x * ⇑g y = ⇑g y * ⇑f x) :
If S' = S ⊗[R] R', then any pair of R-algebra homomorphisms f : S → A and g : R' → A
such that f x and g y commutes for all x, y descends to a (unique) homomoprhism S' → A.
Equations
- algebra.pushout_desc S' f g hf = let _inst : module S A := module.comp_hom A f.to_ring_hom in alg_hom.of_linear_map (linear_map.restrict_scalars R (algebra.is_pushout.out.lift g.to_linear_map)) _ _
@[simp]
theorem
algebra.pushout_desc_left
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
[H : algebra.is_pushout R S R' S']
{A : Type u_2}
[semiring A]
[algebra R A]
(f : S →ₐ[R] A)
(g : R' →ₐ[R] A)
(H_1 : ∀ (x : S) (y : R'), ⇑f x * ⇑g y = ⇑g y * ⇑f x)
(x : S) :
⇑(algebra.pushout_desc S' f g H_1) (⇑(algebra_map S S') x) = ⇑f x
theorem
algebra.lift_alg_hom_comp_left
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
[H : algebra.is_pushout R S R' S']
{A : Type u_2}
[semiring A]
[algebra R A]
(f : S →ₐ[R] A)
(g : R' →ₐ[R] A)
(H_1 : ∀ (x : S) (y : R'), ⇑f x * ⇑g y = ⇑g y * ⇑f x) :
(algebra.pushout_desc S' f g H_1).comp (is_scalar_tower.to_alg_hom R S S') = f
@[simp]
theorem
algebra.pushout_desc_right
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
[H : algebra.is_pushout R S R' S']
{A : Type u_2}
[semiring A]
[algebra R A]
(f : S →ₐ[R] A)
(g : R' →ₐ[R] A)
(H_1 : ∀ (x : S) (y : R'), ⇑f x * ⇑g y = ⇑g y * ⇑f x)
(x : R') :
⇑(algebra.pushout_desc S' f g H_1) (⇑(algebra_map R' S') x) = ⇑g x
theorem
algebra.lift_alg_hom_comp_right
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
[H : algebra.is_pushout R S R' S']
{A : Type u_2}
[semiring A]
[algebra R A]
(f : S →ₐ[R] A)
(g : R' →ₐ[R] A)
(H_1 : ∀ (x : S) (y : R'), ⇑f x * ⇑g y = ⇑g y * ⇑f x) :
(algebra.pushout_desc S' f g H_1).comp (is_scalar_tower.to_alg_hom R R' S') = g
@[ext]
theorem
algebra.is_pushout.alg_hom_ext
{R : Type u_1}
{S : Type v₃}
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_6}
(S' : Type u_7)
[comm_ring R']
[comm_ring S']
[algebra R R']
[algebra S S']
[algebra R' S']
[algebra R S']
[is_scalar_tower R R' S']
[is_scalar_tower R S S']
[H : algebra.is_pushout R S R' S']
{A : Type u_2}
[semiring A]
[algebra R A]
{f g : S' →ₐ[R] A}
(h₁ : f.comp (is_scalar_tower.to_alg_hom R R' S') = g.comp (is_scalar_tower.to_alg_hom R R' S'))
(h₂ : f.comp (is_scalar_tower.to_alg_hom R S S') = g.comp (is_scalar_tower.to_alg_hom R S S')) :
f = g