Documentation

Mathlib.Algebra.Algebra.Quasispectrum

Quasiregularity and quasispectrum #

For a non-unital ring R, an element r : R is quasiregular if it is invertible in the monoid (R, ∘) where x ∘ y := y + x + x * y with identity 0 : R. We implement this both as a type synonym PreQuasiregular which has an associated Monoid instance (note: not an AddMonoid instance despite the fact that 0 : R is the identity in this monoid) so that one may access the quasiregular elements of R as (PreQuasiregular R)ˣ, but also as a predicate IsQuasiregular.

Quasiregularity is closely tied to invertibility. Indeed, (PreQuasiregular A)ˣ is isomorphic to the subgroup of Unitization R A whose scalar part is 1, whenever A is a non-unital R-algebra, and moreover this isomorphism is implemented by the map (x : A) ↦ (1 + x : Unitization R A). It is because of this isomorphism, and the associated ties with multiplicative invertibility, that we choose a Monoid (as opposed to an AddMonoid) structure on PreQuasiregular. In addition, in unital rings, we even have IsQuasiregular x ↔ IsUnit (1 + x).

The quasispectrum of a : A (with respect to R) is defined in terms of quasiregularity, and this is the natural analogue of the spectrum for non-unital rings. Indeed, it is true that quasispectrum R a = spectrum R a ∪ {0} when A is unital.

In Mathlib, the quasispectrum is the domain of the continuous functions associated to the non-unital continuous functional calculus.

Main definitions #

Main theorems #

structure PreQuasiregular (R : Type u_1) :
Type u_1

A type synonym for non-unital rings where an alternative monoid structure is introduced. If R is a non-unital semiring, then PreQuasiregular R is equipped with the monoid structure with binary operation fun x y ↦ y + x + x * y and identity 0. Elements of R which are invertible in this monoid satisfy the predicate IsQuasiregular.

Instances For
    @[simp]
    theorem PreQuasiregular.equiv_apply_val {R : Type u_1} (val : R) :
    (PreQuasiregular.equiv val).val = val
    @[simp]
    theorem PreQuasiregular.equiv_symm_apply {R : Type u_1} (self : PreQuasiregular R) :
    PreQuasiregular.equiv.symm self = self.val

    The identity map between R and PreQuasiregular R.

    Equations
    • PreQuasiregular.equiv = { toFun := PreQuasiregular.mk, invFun := PreQuasiregular.val, left_inv := , right_inv := }
    Instances For
      Equations
      • PreQuasiregular.instOne = { one := PreQuasiregular.equiv 0 }
      Equations
      • PreQuasiregular.instMul = { mul := fun (x y : PreQuasiregular R) => { val := y.val + x.val + x.val * y.val } }
      @[simp]
      theorem PreQuasiregular.val_mul {R : Type u_1} [NonUnitalSemiring R] (x : PreQuasiregular R) (y : PreQuasiregular R) :
      (x * y).val = y.val + x.val + x.val * y.val
      Equations
      • PreQuasiregular.instMonoid = Monoid.mk npowRec
      @[simp]
      theorem PreQuasiregular.inv_add_add_mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] (u : (PreQuasiregular R)ˣ) :
      (↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0
      @[simp]
      theorem PreQuasiregular.add_inv_add_mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] (u : (PreQuasiregular R)ˣ) :
      (↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0

      The subgroup of the units of Unitization R A whose scalar part is 1.

      Equations
      Instances For
        @[simp]
        theorem Unitization.mem_unitsFstOne {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : (Unitization R A)ˣ} :
        x Unitization.unitsFstOne R A (↑x).fst = 1
        @[simp]
        theorem Unitization.unitsFstOne_val_val_fst {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (Unitization.unitsFstOne R A)) :
        (↑x).fst = 1
        @[simp]
        theorem Unitization.unitsFstOne_val_inv_val_fst {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (Unitization.unitsFstOne R A)) :
        (↑(↑x)⁻¹).fst = 1
        @[simp]
        theorem Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (PreQuasiregular A)ˣ) :
        ((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x) = 1 + (PreQuasiregular.equiv.symm x)
        @[simp]
        theorem Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (Unitization.unitsFstOne R A)) :
        ((Unitization.unitsFstOne_mulEquiv_quasiregular R) x) = PreQuasiregular.equiv (↑x).snd
        @[simp]

        If A is a non-unital R-algebra, then the subgroup of units of Unitization R A whose scalar part is 1 : R (i.e., Unitization.unitsFstOne) is isomorphic to the group of units of PreQuasiregular A.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def IsQuasiregular {R : Type u_1} [NonUnitalSemiring R] (x : R) :

          In a non-unital semiring R, an element x : R satisfies IsQuasiregular if it is a unit under the monoid operation fun x y ↦ y + x + x * y.

          Equations
          Instances For
            theorem isQuasiregular_iff {R : Type u_1} [NonUnitalSemiring R] {x : R} :
            IsQuasiregular x ∃ (y : R), y + x + x * y = 0 x + y + y * x = 0
            theorem IsQuasiregular.map {F : Type u_1} {R : Type u_2} {S : Type u_3} [NonUnitalSemiring R] [NonUnitalSemiring S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x : R} (hx : IsQuasiregular x) :
            theorem IsQuasiregular.isUnit_one_add {R : Type u_1} [Semiring R] {x : R} (hx : IsQuasiregular x) :
            IsUnit (1 + x)
            theorem isQuasiregular_iff_isUnit {R : Type u_1} [Ring R] {x : R} :
            theorem isQuasiregular_iff_isUnit' (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} :
            def quasispectrum (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] (a : A) :
            Set R

            If A is a non-unital R-algebra, the R-quasispectrum of a : A consists of those r : R such that if r is invertible (in R), then -(r⁻¹ • a) is not quasiregular.

            The quasispectrum is precisely the spectrum in the unitization when R is a commutative ring. See Unitization.quasispectrum_eq_spectrum_inr.

            Equations
            Instances For
              theorem quasispectrum.not_isUnit_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] (a : A) {r : R} (hr : ¬IsUnit r) :
              @[simp]
              theorem quasispectrum.zero_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) :
              instance quasispectrum.instZero (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) :
              Equations
              theorem NonUnitalAlgHom.quasispectrum_apply_subset' {F : Type u_3} {R : Type u_4} (S : Type u_5) {A : Type u_6} {B : Type u_7} [CommSemiring R] [CommRing S] [NonUnitalRing A] [NonUnitalRing B] [Module R S] [Module S A] [Module R A] [Module S B] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B] [FunLike F A B] [NonUnitalAlgHomClass F S A B] (φ : F) (a : A) :

              A version of NonUnitalAlgHom.quasispectrum_apply_subset which allows for quasispectrum R, where R is a semiring, but φ must still function over a scalar ring S. In this case, we need S to be explicit. The primary use case is, for instance, R := ℝ≥0 and S := ℝ or S := ℂ.

              theorem NonUnitalAlgHom.quasispectrum_apply_subset {F : Type u_3} {R : Type u_4} {A : Type u_5} {B : Type u_6} [CommRing R] [NonUnitalRing A] [NonUnitalRing B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (a : A) :

              If φ is non-unital algebra homomorphism over a scalar ring R, then quasispectrum R (φ a) ⊆ quasispectrum R a.

              @[simp]
              theorem quasispectrum.coe_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) :
              0 = 0
              theorem quasispectrum.mem_of_not_quasiregular {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] (a : A) {r : Rˣ} (hr : ¬IsQuasiregular (-(r⁻¹ a))) :
              theorem quasispectrum_eq_spectrum_union (R : Type u_3) {A : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] (a : A) :
              quasispectrum R a = spectrum R a {r : R | ¬IsUnit r}
              theorem spectrum_subset_quasispectrum (R : Type u_3) {A : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] (a : A) :
              theorem quasispectrum_eq_spectrum_union_zero (R : Type u_3) {A : Type u_4} [Semifield R] [Ring A] [Algebra R A] (a : A) :
              theorem mem_quasispectrum_iff {R : Type u_3} {A : Type u_4} [Semifield R] [Ring A] [Algebra R A] {a : A} {x : R} :
              theorem Unitization.zero_mem_spectrum_inr (R : Type u_3) (S : Type u_4) {A : Type u_5} [CommSemiring R] [CommRing S] [Nontrivial S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) :
              0 spectrum R a
              theorem Unitization.mem_spectrum_inr_of_not_isUnit {R : Type u_3} {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) (r : R) (hr : ¬IsUnit r) :
              r spectrum R a
              theorem Unitization.quasispectrum_eq_spectrum_inr (R : Type u_3) {A : Type u_4} [CommRing R] [Ring A] [Algebra R A] (a : A) :
              theorem Unitization.quasispectrum_eq_spectrum_inr' (R : Type u_3) (S : Type u_4) {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) :
              class NonnegSpectrumClass (𝕜 : Type u_3) (A : Type u_4) [OrderedCommSemiring 𝕜] [NonUnitalRing A] [PartialOrder A] [Module 𝕜 A] :

              A class for 𝕜-algebras with a partial order where the ordering is compatible with the (quasi)spectrum.

              • quasispectrum_nonneg_of_nonneg : ∀ (a : A), 0 axquasispectrum 𝕜 a, 0 x
              Instances
                theorem NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg {𝕜 : Type u_3} {A : Type u_4} :
                ∀ {inst : OrderedCommSemiring 𝕜} {inst_1 : NonUnitalRing A} {inst_2 : PartialOrder A} {inst_3 : Module 𝕜 A} [self : NonnegSpectrumClass 𝕜 A] (a : A), 0 axquasispectrum 𝕜 a, 0 x
                theorem NonnegSpectrumClass.iff_spectrum_nonneg {𝕜 : Type u_3} {A : Type u_4} [LinearOrderedSemifield 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] :
                NonnegSpectrumClass 𝕜 A ∀ (a : A), 0 axspectrum 𝕜 a, 0 x
                theorem NonnegSpectrumClass.of_spectrum_nonneg {𝕜 : Type u_3} {A : Type u_4} [LinearOrderedSemifield 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] :
                (∀ (a : A), 0 axspectrum 𝕜 a, 0 x)NonnegSpectrumClass 𝕜 A

                Alias of the reverse direction of NonnegSpectrumClass.iff_spectrum_nonneg.

                theorem spectrum_nonneg_of_nonneg {𝕜 : Type u_3} {A : Type u_4} [OrderedCommSemiring 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] ⦃a : A (ha : 0 a) ⦃x : 𝕜 (hx : x spectrum 𝕜 a) :
                0 x

                Restriction of the spectrum #

                structure QuasispectrumRestricts {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] (a : A) (f : SR) :

                Given an element a : A of an S-algebra, where S is itself an R-algebra, we say that the spectrum of a restricts via a function f : S → R if f is a left inverse of algebraMap R S, and f is a right inverse of algebraMap R S on spectrum S a.

                For example, when f = Complex.re (so S := ℂ and R := ℝ), SpectrumRestricts a f means that the -spectrum of a is contained within . This arises naturally when a is selfadjoint and A is a C⋆-algebra.

                This is the property allows us to restrict a continuous functional calculus over S to a continuous functional calculus over R.

                Instances For
                  theorem QuasispectrumRestricts.rightInvOn {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} (self : QuasispectrumRestricts a f) :

                  f is a right inverse of algebraMap R S when restricted to quasispectrum S a.

                  theorem QuasispectrumRestricts.left_inv {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} (self : QuasispectrumRestricts a f) :

                  f is a left inverse of algebraMap R S.

                  theorem quasispectrumRestricts_iff {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] (a : A) (f : SR) :
                  @[simp]
                  theorem quasispectrum.algebraMap_mem_iff (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} {r : R} :
                  theorem quasispectrum.algebraMap_mem (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} {r : R} :

                  Alias of the reverse direction of quasispectrum.algebraMap_mem_iff.

                  theorem quasispectrum.of_algebraMap_mem (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} {r : R} :

                  Alias of the forward direction of quasispectrum.algebraMap_mem_iff.

                  @[simp]
                  theorem quasispectrum.preimage_algebraMap (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} :
                  theorem QuasispectrumRestricts.map_zero {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} (h : QuasispectrumRestricts a f) :
                  f 0 = 0
                  theorem QuasispectrumRestricts.of_subset_range_algebraMap {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} (hf : Function.LeftInverse f (algebraMap R S)) (h : quasispectrum S a Set.range (algebraMap R S)) :
                  theorem QuasispectrumRestricts.of_quasispectrum_eq {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {b : A} {f : SR} (ha : QuasispectrumRestricts a f) (h : quasispectrum S a = quasispectrum S b) :
                  theorem QuasispectrumRestricts.algebraMap_image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) :
                  theorem QuasispectrumRestricts.image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) :
                  theorem QuasispectrumRestricts.apply_mem {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) {s : S} (hs : s quasispectrum S a) :
                  theorem QuasispectrumRestricts.subset_preimage {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : SR} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) :
                  theorem QuasispectrumRestricts.comp {R₁ : Type u_6} {R₂ : Type u_7} {R₃ : Type u_8} {A : Type u_9} [Semifield R₁] [Field R₂] [Field R₃] [NonUnitalRing A] [Module R₁ A] [Module R₂ A] [Module R₃ A] [Algebra R₁ R₂] [Algebra R₂ R₃] [Algebra R₁ R₃] [IsScalarTower R₁ R₂ R₃] [IsScalarTower R₂ R₃ A] [IsScalarTower R₃ A A] [SMulCommClass R₃ A A] {a : A} {f : R₃R₂} {g : R₂R₁} {e : R₃R₁} (hfge : g f = e) (hf : QuasispectrumRestricts a f) (hg : QuasispectrumRestricts a g) :
                  @[reducible]
                  def SpectrumRestricts {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R A] [Algebra S A] [Algebra R S] (a : A) (f : SR) :

                  A (reducible) alias of QuasispectrumRestricts which enforces stronger type class assumptions on the types involved, as it's really intended for the spectrum. The separate definition also allows for dot notation.

                  Equations
                  Instances For
                    theorem SpectrumRestricts.rightInvOn {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} (h : SpectrumRestricts a f) :
                    theorem SpectrumRestricts.of_rightInvOn {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} (h₁ : Function.LeftInverse f (algebraMap R S)) (h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)) :
                    theorem spectrumRestricts_iff {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} :
                    theorem SpectrumRestricts.of_subset_range_algebraMap {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} (hf : Function.LeftInverse f (algebraMap R S)) (h : spectrum S a Set.range (algebraMap R S)) :
                    theorem SpectrumRestricts.of_spectrum_eq {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {b : A} {f : SR} (ha : SpectrumRestricts a f) (h : spectrum S a = spectrum S b) :
                    theorem SpectrumRestricts.algebraMap_image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} [IsScalarTower R S A] (h : SpectrumRestricts a f) :
                    (algebraMap R S) '' spectrum R a = spectrum S a
                    theorem SpectrumRestricts.image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} [IsScalarTower R S A] (h : SpectrumRestricts a f) :
                    f '' spectrum S a = spectrum R a
                    theorem SpectrumRestricts.apply_mem {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} [IsScalarTower R S A] (h : SpectrumRestricts a f) {s : S} (hs : s spectrum S a) :
                    f s spectrum R a
                    theorem SpectrumRestricts.subset_preimage {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} [IsScalarTower R S A] (h : SpectrumRestricts a f) :
                    theorem quasispectrumRestricts_iff_spectrumRestricts_inr (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] {a : A} {f : SR} :
                    theorem quasispectrumRestricts_iff_spectrumRestricts {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : SR} :