Documentation

Mathlib.Algebra.Algebra.Basic

Algebras over commutative semirings #

In this file we define associative unital Algebras over commutative (semi)rings.

See the implementation notes for remarks about non-associative and non-unital algebras.

Main definitions: #

Implementation notes #

Given a commutative (semi)ring R, there are two ways to define an R-algebra structure on a (possibly noncommutative) (semi)ring A:

We define Algebra R A in a way that subsumes both definitions, by extending SMul R A and requiring that this scalar action r • x must agree with left multiplication by the image of the structure morphism algebraMap R A r * x.

As a result, there are two ways to talk about an R-algebra A when A is a semiring:

  1. variable [CommSemiring R] [Semiring A]
    variable [Algebra R A]
    
  2. variable [CommSemiring R] [Semiring A]
    variable [Module R A] [SMulCommClass R A A] [IsScalarTower R A A]
    

The first approach implies the second via typeclass search; so any lemma stated with the second set of arguments will automatically apply to the first set. Typeclass search does not know that the second approach implies the first, but this can be shown with:

example {R A : Type*} [CommSemiring R] [Semiring A]
  [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : Algebra R A :=
Algebra.ofModule smul_mul_assoc mul_smul_comm

The advantage of the first approach is that algebraMap R A is available, and AlgHom R A B and Subalgebra R A can be used. For concrete R and A, algebraMap R A is often definitionally convenient.

The advantage of the second approach is that CommSemiring R, Semiring A, and Module R A can all be relaxed independently; for instance, this allows us to:

While AlgHom R A B cannot be used in the second approach, NonUnitalAlgHom R A B still can.

You should always use the first approach when working with associative unital algebras, and mimic the second approach only when you need to weaken a condition on either R or A.

class Algebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] extends SMul , RingHom :
Type (max u v)

An associative unital R-algebra is a semiring A equipped with a map into its center R → A.

See the implementation notes in this file for discussion of the details of this definition.

  • smul : RAA
  • toFun : RA
  • map_one' : Algebra.toRingHom.toFun 1 = 1
  • map_mul' : ∀ (x y : R), Algebra.toRingHom.toFun (x * y) = Algebra.toRingHom.toFun x * Algebra.toRingHom.toFun y
  • map_zero' : Algebra.toRingHom.toFun 0 = 0
  • map_add' : ∀ (x y : R), Algebra.toRingHom.toFun (x + y) = Algebra.toRingHom.toFun x + Algebra.toRingHom.toFun y
  • commutes' : ∀ (r : R) (x : A), Algebra.toRingHom r * x = x * Algebra.toRingHom r
  • smul_def' : ∀ (r : R) (x : A), r x = Algebra.toRingHom r * x
Instances
    def algebraMap (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :
    R →+* A

    Embedding R →+* A given by Algebra structure.

    Equations
    Instances For
      def Algebra.cast {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
      RA

      Coercion from a commutative semiring to an algebra over this semiring.

      Equations
      Instances For
        def algebraMap.coeHTCT (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] :
        Equations
        Instances For
          @[simp]
          theorem algebraMap.coe_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
          0 = 0
          @[simp]
          theorem algebraMap.coe_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
          1 = 1
          theorem algebraMap.coe_add {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : R) (b : R) :
          (a + b) = a + b
          theorem algebraMap.coe_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : R) (b : R) :
          (a * b) = a * b
          theorem algebraMap.coe_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (a : R) (n : ) :
          (a ^ n) = a ^ n
          theorem algebraMap.coe_neg {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (x : R) :
          (-x) = -x
          theorem algebraMap.coe_prod {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type u_3} {s : Finset ι} (a : ιR) :
          (Finset.prod s fun (i : ι) => a i) = Finset.prod s fun (i : ι) => (a i)
          theorem algebraMap.coe_sum {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {ι : Type u_3} {s : Finset ι} (a : ιR) :
          (Finset.sum s fun (i : ι) => a i) = Finset.sum s fun (i : ι) => (a i)
          @[simp]
          theorem algebraMap.coe_inj {R : Type u_1} {A : Type u_2} [Field R] [CommSemiring A] [Nontrivial A] [Algebra R A] {a : R} {b : R} :
          a = b a = b
          @[simp]
          theorem algebraMap.lift_map_eq_zero_iff {R : Type u_1} {A : Type u_2} [Field R] [CommSemiring A] [Nontrivial A] [Algebra R A] (a : R) :
          a = 0 a = 0
          theorem algebraMap.coe_inv {R : Type u_1} (A : Type u_2) [Semifield R] [DivisionSemiring A] [Algebra R A] (r : R) :
          r⁻¹ = (r)⁻¹
          theorem algebraMap.coe_div {R : Type u_1} (A : Type u_2) [Semifield R] [DivisionSemiring A] [Algebra R A] (r : R) (s : R) :
          (r / s) = r / s
          theorem algebraMap.coe_zpow {R : Type u_1} (A : Type u_2) [Semifield R] [DivisionSemiring A] [Algebra R A] (r : R) (z : ) :
          (r ^ z) = r ^ z
          theorem algebraMap.coe_ratCast (R : Type u_1) (A : Type u_2) [Field R] [DivisionRing A] [Algebra R A] (q : ) :
          q = q
          def RingHom.toAlgebra' {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] (i : R →+* S) (h : ∀ (c : R) (x : S), i c * x = x * i c) :

          Creating an algebra from a morphism to the center of a semiring.

          Equations
          Instances For
            def RingHom.toAlgebra {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (i : R →+* S) :

            Creating an algebra from a morphism to a commutative semiring.

            Equations
            Instances For
              theorem RingHom.algebraMap_toAlgebra {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (i : R →+* S) :
              @[reducible]
              def Algebra.ofModule' {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Module R A] (h₁ : ∀ (r : R) (x : A), r 1 * x = r x) (h₂ : ∀ (r : R) (x : A), x * r 1 = r x) :

              Let R be a commutative semiring, let A be a semiring with a Module R structure. If (r • 1) * x = x * (r • 1) = r • x for all r : R and x : A, then A is an Algebra over R.

              See note [reducible non-instances].

              Equations
              • Algebra.ofModule' h₁ h₂ = Algebra.mk { toMonoidHom := { toOneHom := { toFun := fun (r : R) => r 1, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
              Instances For
                @[reducible]
                def Algebra.ofModule {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Module R A] (h₁ : ∀ (r : R) (x y : A), r x * y = r (x * y)) (h₂ : ∀ (r : R) (x y : A), x * r y = r (x * y)) :

                Let R be a commutative semiring, let A be a semiring with a Module R structure. If (r • x) * y = x * (r • y) = r • (x * y) for all r : R and x y : A, then A is an Algebra over R.

                See note [reducible non-instances].

                Equations
                Instances For
                  theorem Algebra.algebra_ext {R : Type u_2} [CommSemiring R] {A : Type u_3} [Semiring A] (P : Algebra R A) (Q : Algebra R A) (h : ∀ (r : R), (algebraMap R A) r = (algebraMap R A) r) :
                  P = Q

                  To prove two algebra structures on a fixed [CommSemiring R] [Semiring A] agree, it suffices to check the algebraMaps agree.

                  instance Algebra.toModule {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
                  Module R A
                  Equations
                  theorem Algebra.smul_def {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
                  r x = (algebraMap R A) r * x
                  theorem Algebra.algebraMap_eq_smul_one {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
                  (algebraMap R A) r = r 1
                  theorem Algebra.algebraMap_eq_smul_one' {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
                  (algebraMap R A) = fun (r : R) => r 1
                  theorem Algebra.commutes {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
                  (algebraMap R A) r * x = x * (algebraMap R A) r

                  mul_comm for Algebras when one element is from the base ring.

                  theorem Algebra.commute_algebraMap_left {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
                  Commute ((algebraMap R A) r) x
                  theorem Algebra.commute_algebraMap_right {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) :
                  Commute x ((algebraMap R A) r)
                  theorem Algebra.left_comm {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) (y : A) :
                  x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)

                  mul_left_comm for Algebras when one element is from the base ring.

                  theorem Algebra.right_comm {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) (y : A) :
                  x * (algebraMap R A) r * y = x * y * (algebraMap R A) r

                  mul_right_comm for Algebras when one element is from the base ring.

                  instance IsScalarTower.right {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
                  Equations
                  • =
                  @[simp]
                  theorem RingHom.smulOneHom_eq_algebraMap {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
                  RingHom.smulOneHom = algebraMap R A
                  @[simp]
                  theorem Algebra.mul_smul_comm {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (s : R) (x : A) (y : A) :
                  x * s y = s (x * y)

                  This is just a special case of the global mul_smul_comm lemma that requires less typeclass search (and was here first).

                  @[simp]
                  theorem Algebra.smul_mul_assoc {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) (x : A) (y : A) :
                  r x * y = r (x * y)

                  This is just a special case of the global smul_mul_assoc lemma that requires less typeclass search (and was here first).

                  @[simp]
                  theorem smul_algebraMap {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] {α : Type u_2} [Monoid α] [MulDistribMulAction α A] [SMulCommClass α R A] (a : α) (r : R) :
                  a (algebraMap R A) r = (algebraMap R A) r
                  def Algebra.linearMap (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] :

                  The canonical ring homomorphism algebraMap R A : R →+* A for any R-algebra A, packaged as an R-linear map.

                  Equations
                  Instances For
                    @[simp]
                    theorem Algebra.linearMap_apply (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
                    theorem Algebra.coe_linearMap (R : Type u) (A : Type w) [CommSemiring R] [Semiring A] [Algebra R A] :
                    (Algebra.linearMap R A) = (algebraMap R A)
                    instance Algebra.id (R : Type u) [CommSemiring R] :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    theorem Algebra.id.map_eq_self {R : Type u} [CommSemiring R] (x : R) :
                    (algebraMap R R) x = x
                    @[simp]
                    theorem Algebra.id.smul_eq_mul {R : Type u} [CommSemiring R] (x : R) (y : R) :
                    x y = x * y
                    Equations
                    • PUnit.algebra = Algebra.mk { toMonoidHom := { toOneHom := { toFun := fun (x : R) => PUnit.unit, map_one' := }, map_mul' := }, map_zero' := , map_add' := }
                    instance ULift.algebra {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    theorem ULift.algebraMap_eq {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
                    (algebraMap R (ULift.{u_2, w} A)) r = { down := (algebraMap R A) r }
                    @[simp]
                    theorem ULift.down_algebraMap {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
                    ((algebraMap R (ULift.{u_2, w} A)) r).down = (algebraMap R A) r
                    instance Algebra.ofSubsemiring {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subsemiring R) :
                    Algebra (S) A

                    Algebra over a subsemiring. This builds upon Subsemiring.module.

                    Equations
                    theorem Algebra.coe_algebraMap_ofSubsemiring {R : Type u} [CommSemiring R] (S : Subsemiring R) :
                    (algebraMap (S) R) = Subtype.val
                    theorem Algebra.algebraMap_ofSubsemiring_apply {R : Type u} [CommSemiring R] (S : Subsemiring R) (x : S) :
                    (algebraMap (S) R) x = x
                    instance Algebra.ofSubring {R : Type u_2} {A : Type u_3} [CommRing R] [Ring A] [Algebra R A] (S : Subring R) :
                    Algebra (S) A

                    Algebra over a subring. This builds upon Subring.module.

                    Equations
                    theorem Algebra.coe_algebraMap_ofSubring {R : Type u_2} [CommRing R] (S : Subring R) :
                    (algebraMap (S) R) = Subtype.val
                    theorem Algebra.algebraMap_ofSubring_apply {R : Type u_2} [CommRing R] (S : Subring R) (x : S) :
                    (algebraMap (S) R) x = x
                    def Algebra.algebraMapSubmonoid {R : Type u} [CommSemiring R] (S : Type u_2) [Semiring S] [Algebra R S] (M : Submonoid R) :

                    Explicit characterization of the submonoid map in the case of an algebra. S is made explicit to help with type inference

                    Equations
                    Instances For
                      theorem Algebra.mul_sub_algebraMap_commutes {R : Type u} {A : Type w} [CommSemiring R] [Ring A] [Algebra R A] (x : A) (r : R) :
                      x * (x - (algebraMap R A) r) = (x - (algebraMap R A) r) * x
                      theorem Algebra.mul_sub_algebraMap_pow_commutes {R : Type u} {A : Type w} [CommSemiring R] [Ring A] [Algebra R A] (x : A) (r : R) (n : ) :
                      x * (x - (algebraMap R A) r) ^ n = (x - (algebraMap R A) r) ^ n * x
                      @[reducible]
                      def Algebra.semiringToRing (R : Type u) {A : Type w} [CommRing R] [Semiring A] [Algebra R A] :

                      A Semiring that is an Algebra over a commutative ring carries a natural Ring structure. See note [reducible non-instances].

                      Equations
                      Instances For
                        instance Module.End.instAlgebra (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] :
                        Equations
                        theorem Module.algebraMap_end_eq_smul_id (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] (a : R) :
                        (algebraMap R (Module.End S M)) a = a LinearMap.id
                        @[simp]
                        theorem Module.algebraMap_end_apply (R : Type u) (S : Type v) (M : Type w) [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] (a : R) (m : M) :
                        ((algebraMap R (Module.End S M)) a) m = a m
                        @[simp]
                        theorem Module.ker_algebraMap_end (K : Type u) (V : Type v) [Field K] [AddCommGroup V] [Module K V] (a : K) (ha : a 0) :
                        theorem Module.End_algebraMap_isUnit_inv_apply_eq_iff {R : Type u} (S : Type v) {M : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (Module.End S M)) x)) (m : M) (m' : M) :
                        (IsUnit.unit h)⁻¹ m = m' m = x m'
                        theorem Module.End_algebraMap_isUnit_inv_apply_eq_iff' {R : Type u} (S : Type v) {M : Type w} [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] {x : R} (h : IsUnit ((algebraMap R (Module.End S M)) x)) (m : M) (m' : M) :
                        m' = (IsUnit.unit h)⁻¹ m m = x m'
                        theorem LinearMap.map_algebraMap_mul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) :
                        f ((algebraMap R A) r * a) = (algebraMap R B) r * f a

                        An alternate statement of LinearMap.map_smul for when algebraMap is more convenient to work with than .

                        theorem LinearMap.map_mul_algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (a : A) (r : R) :
                        f (a * (algebraMap R A) r) = f a * (algebraMap R B) r
                        instance algebraNat {R : Type u_1} [Semiring R] :

                        Semiring ⥤ ℕ-Alg

                        Equations
                        Equations
                        • =
                        @[simp]
                        theorem RingHom.map_rat_algebraMap {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [Algebra R] [Algebra S] (f : R →+* S) (r : ) :
                        f ((algebraMap R) r) = (algebraMap S) r
                        instance algebraRat {α : Type u_1} [DivisionRing α] [CharZero α] :
                        Equations
                        Equations
                        • =
                        instance algebraInt (R : Type u_1) [Ring R] :

                        Ring ⥤ ℤ-Alg

                        Equations
                        @[simp]

                        A special case of eq_intCast' that happens to be true definitionally

                        Equations
                        • =

                        If algebraMap R A is injective and A has no zero divisors, R-multiples in A are zero only if one of the factors is zero.

                        Cannot be an instance because there is no Injective (algebraMap R A) typeclass.

                        theorem NeZero.of_noZeroSMulDivisors (R : Type u_1) (A : Type u_2) (n : ) [CommRing R] [NeZero n] [Ring A] [Nontrivial A] [Algebra R A] [NoZeroSMulDivisors R A] :
                        NeZero n
                        theorem algebra_compatible_smul {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (m : M) :
                        r m = (algebraMap R A) r m
                        @[simp]
                        theorem algebraMap_smul {R : Type u_1} [CommSemiring R] (A : Type u_2) [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (m : M) :
                        (algebraMap R A) r m = r m
                        theorem intCast_smul {k : Type u_5} {V : Type u_6} [CommRing k] [AddCommGroup V] [Module k V] (r : ) (x : V) :
                        r x = r x
                        theorem NoZeroSMulDivisors.trans (R : Type u_5) (A : Type u_6) (M : Type u_7) [CommRing R] [Ring A] [IsDomain A] [Algebra R A] [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors R A] [NoZeroSMulDivisors A M] :
                        instance IsScalarTower.to_smulCommClass {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] :
                        Equations
                        • =
                        instance IsScalarTower.to_smulCommClass' {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] :
                        Equations
                        • =
                        instance Algebra.to_smulCommClass {R : Type u_5} {A : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] :
                        Equations
                        • =
                        theorem smul_algebra_smul_comm {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {M : Type u_3} [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (r : R) (a : A) (m : M) :
                        a r m = r a m
                        def LinearMap.ltoFun (R : Type u) (M : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A] [Algebra R A] :
                        (M →ₗ[R] A) →ₗ[A] MA

                        A-linearly coerce an R-linear map from M to A to a function, given an algebra A over a commutative semiring R and M a module over R.

                        Equations
                        Instances For

                          TODO: The following lemmas no longer involve Algebra at all, and could be moved closer to Algebra/Module/Submodule.lean. Currently this is tricky because ker, range, , and are all defined in LinearAlgebra/Basic.lean.

                          @[simp]
                          theorem LinearMap.ker_restrictScalars (R : Type u_1) {S : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[S] N) :
                          @[inline, reducible]
                          abbrev Invertible.algebraMapOfInvertibleAlgebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : Invertible ((algebraMap R A) r)) :

                          If there is a linear map f : A →ₗ[R] B that preserves 1, then algebraMap R B r is invertible when algebraMap R A r is.

                          Equations
                          Instances For
                            theorem IsUnit.algebraMap_of_algebraMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (hf : f 1 = 1) {r : R} (h : IsUnit ((algebraMap R A) r)) :
                            IsUnit ((algebraMap R B) r)

                            If there is a linear map f : A →ₗ[R] B that preserves 1, then algebraMap R B r is a unit when algebraMap R A r is.