Theorems · Theorem · commutative algebra

Algebra.IsEffective.eqLocus_includeLeft_includeRight

∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S],
  Algebra.IsEffective R S →
    ↑(Algebra.TensorProduct.includeLeftRingHom.eqLocus Algebra.TensorProduct.includeRight.toRingHom) =
      Set.range ⇑(algebraMap R S)

If IsEffective R S is true, then the equalizer of s ↦ s ⊗ₜ 1 : S →+* S ⊗[R] S and s ↦ 1 ⊗ₜ s : S →+* S ⊗[R] S is the image of algebraMap R S : R →+* S.

Defined in

Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringRingAlgebra