Theorems · Theorem · ring theory

GradedTensorProduct.algHom_ext

∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {C : Type u_5} [inst_10 : Ring C] [inst_11 : Algebra R C]
  ⦃f g : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C⦄,
  f.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) = g.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) →
    f.comp (GradedTensorProduct.includeRight 𝒜 ℬ) = g.comp (GradedTensorProduct.includeRight 𝒜 ℬ) → f = g

Two algebra morphism from the graded tensor product agree if their compositions with the left and right inclusions agree.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidableEqCommRingRingRingAlgebraAlgebraGradedAlgebraGradedAlgebraModuleRingAlgebra