Algebras which are commutative ring epimorphisms

class Algebra.IsEpi (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : Prop

A commutative R-algebra A is epi, if the multiplication map A ⊗[R] A → A is injective.

• injective_lift_mul : Function.Injective ⇑(_root_.TensorProduct.lift (LinearMap.mul R A))

theorem Algebra.isEpi_iff_forall_one_tmul_eq (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra.IsEpi R A ↔ ∀ (a : A), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1

See also CommRingCat.epi_iff_epi.

theorem Algebra.isEpi_of_surjective_algebraMap (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (h : Function.Surjective ⇑(algebraMap R A)) : Algebra.IsEpi R A

See also Algebra.isEpi_iff_surjective_algebraMap_of_finite.

instance Algebra.instIsEpiOfIsDomainOfIsFractionRing (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [Field A] [Algebra R A] [IsFractionRing R A] : Algebra.IsEpi R A

theorem Algebra.isEpi_iff_surjective_algebraMap_of_finite {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Module.Finite R A] : Algebra.IsEpi R A ↔ Function.Surjective ⇑(algebraMap R A)

@[deprecated Algebra.isEpi_iff_surjective_algebraMap_of_finite (since := "2026-01-13")]

theorem RingHom.surjective_of_tmul_eq_tmul_of_finite {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] [Module.Finite R A] : Algebra.IsEpi R A ↔ Function.Surjective ⇑(algebraMap R A)

Alias of Algebra.isEpi_iff_surjective_algebraMap_of_finite.

theorem Algebra.tmul_comm (R : Type u_1) {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] [Algebra.IsEpi R A] (a b : A) : a ⊗ₜ[R] b = b ⊗ₜ[R] a

theorem Algebra.injective_lift_lsmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] [Algebra.IsEpi R A] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] : Function.Injective ⇑(_root_.TensorProduct.lift (LinearMap.restrictScalars₁₂ R R (LinearMap.lsmul A M)))

If an R-algebra A is epi, then the scalar multiplication A ⊗[R] M → M is injective, for any A-module M.

noncomputable def TensorProduct.lid' (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] [Algebra.IsEpi R A] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] : TensorProduct R A M ≃ₗ[A] M

A heterogeneous variant of TensorProduct.lid when R → A is epi.

Equations

• TensorProduct.lid' R A M = LinearEquiv.ofBijective (TensorProduct.AlgebraTensorModule.lift (LinearMap.restrictScalarsₗ R A M M A ∘ₗ LinearMap.lsmul A M)) ⋯

@[simp]

theorem TensorProduct.lid'_apply_tmul (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] [Algebra.IsEpi R A] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (a : A) (m : M) : (lid' R A M) (a ⊗ₜ[R] m) = a • m

@[simp]

theorem TensorProduct.lid'_symm_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] [Algebra.IsEpi R A] (M : Type u_3) [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] (m : M) : (lid' R A M).symm m = 1 ⊗ₜ[R] m