Theorems · Theorem · ring theory

GradedTensorProduct.hom_ext_iff

∀ {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 ℬ] {M : Type u_5}
  [inst_9 : AddCommMonoid M] [inst_10 : Module R M] {f g : GradedTensorProduct R 𝒜 ℬ →ₗ[R] M},
  f = g ↔ f ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ) = g ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ)

Defined in

Mathlib.LinearAlgebra.TensorProduct.Graded.Internal

Cited by

0 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringDecidableEqCommRingRingRingAlgebraAlgebraGradedAlgebraGradedAlgebraAddCommMonoidModule