Documentation

Mathlib.Algebra.Algebra.Hom.Rat

Homomorphisms of -algebras #

def RingHom.toRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra R] [Algebra S] (f : R →+* S) :

Reinterpret a RingHom as a -algebra homomorphism. This actually yields an equivalence, see RingHom.equivRatAlgHom.

Equations
  • f.toRatAlgHom = { toRingHom := f, commutes' := }
Instances For
    @[simp]
    theorem RingHom.toRatAlgHom_toRingHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra R] [Algebra S] (f : R →+* S) :
    f.toRatAlgHom = f
    @[simp]
    theorem AlgHom.toRingHom_toRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra R] [Algebra S] (f : R →ₐ[] S) :
    (↑f).toRatAlgHom = f
    @[simp]
    theorem RingHom.equivRatAlgHom_symm_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra R] [Algebra S] (self : R →ₐ[] S) :
    RingHom.equivRatAlgHom.symm self = self.toRingHom
    @[simp]
    theorem RingHom.equivRatAlgHom_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra R] [Algebra S] (f : R →+* S) :
    RingHom.equivRatAlgHom f = f.toRatAlgHom
    def RingHom.equivRatAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra R] [Algebra S] :
    (R →+* S) (R →ₐ[] S)

    The equivalence between RingHom and -algebra homomorphisms.

    Equations
    • RingHom.equivRatAlgHom = { toFun := RingHom.toRatAlgHom, invFun := AlgHom.toRingHom, left_inv := , right_inv := }
    Instances For