Documentation

Mathlib.Algebra.Algebra.Hom.Rat

Homomorphisms of ℚ-algebras #

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

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

Equations
Instances For
    source
    @[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
    source
    @[simp]
    theorem RingHom.toRatAlgHom_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) (x : R) :
    f.toRatAlgHom x = f x
    source
    @[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
    source
    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
    Instances For
      source
      @[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) :
      (equivRatAlgHom R S).symm self = self.toRingHom
      source
      @[simp]
      theorem RingHom.equivRatAlgHom_apply (R : Type u_1) (S : Type u_2) [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) :
      (equivRatAlgHom R S) f = f.toRatAlgHom
      source
      def RingEquiv.toRatAlgEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃+* S) :
      R ≃ₐ[ℚ] S

      Reinterpret a RingEquiv as a ℚ-algebra isomorphism. This actually yields an equivalence, see RingEquiv.equivRatAlgEquiv.

      Equations
      • f.toRatAlgEquiv = { toEquiv := ↑f, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
      Instances For
        source
        theorem RingEquiv.toRatAlgEquiv_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃+* S) (a : R) :
        f.toRatAlgEquiv a = f a
        source
        @[simp]
        theorem RingEquiv.coe_toRatAlgEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃+* S) :
        ⇑f.toRatAlgEquiv = ⇑f
        source
        @[simp]
        theorem RingEquiv.toRingEquiv_toRatAlgEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃+* S) :
        f.toRatAlgEquiv.toRingEquiv = f
        source
        theorem RingEquiv.toAlgHom_toRatAlgEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃+* S) :
        ↑f.toRatAlgEquiv = (↑f).toRatAlgHom
        source
        @[simp]
        theorem RingEquiv.symm_toRatAlgEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃+* S) :
        f.toRatAlgEquiv.symm = f.symm.toRatAlgEquiv
        source
        @[simp]
        theorem AlgEquiv.toRatAlgEquiv_toRingEquiv {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃ₐ[ℚ] S) :
        f.toRingEquiv.toRatAlgEquiv = f
        source
        def RingEquiv.equivRatAlgEquiv (R : Type u_1) (S : Type u_2) [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] :
        R ≃+* S ≃ R ≃ₐ[ℚ] S

        The equivalence between RingEquiv and ℚ-algebra isomorphisms.

        Equations
        Instances For
          source
          @[simp]
          theorem RingEquiv.equivRatAlgEquiv_apply (R : Type u_1) (S : Type u_2) [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (f : R ≃+* S) :
          (equivRatAlgEquiv R S) f = f.toRatAlgEquiv
          source
          @[simp]
          theorem RingEquiv.equivRatAlgEquiv_symm_apply (R : Type u_1) (S : Type u_2) [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] (self : R ≃ₐ[ℚ] S) :
          (equivRatAlgEquiv R S).symm self = self.toRingEquiv
          source
          theorem RingEquiv.toRatAlgEquiv_injective {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] [Algebra ℚ R] [Algebra ℚ S] :
          Function.Injective toRatAlgEquiv