Documentation

Mathlib.Algebra.Algebra.Hom

Homomorphisms of R-algebras #

This file defines bundled homomorphisms of R-algebras.

Main definitions #

Notations #

structure AlgHom (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] extends RingHom , MonoidHom , OneHom , AddMonoidHom , NonUnitalRingHom , MonoidWithZeroHom , MulHom , ZeroHom , AddHom :
Type (max v w)

Defining the homomorphism in the category R-Alg.

    Instances For
      theorem AlgHom.commutes' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (self : A →ₐ[R] B) (r : R) :
      (↑self.toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r

      Defining the homomorphism in the category R-Alg.

      Equations
      Instances For

        Defining the homomorphism in the category R-Alg.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          AlgHomClass F R A B asserts F is a type of bundled algebra homomorphisms from A to B.

            Instances
              theorem AlgHomClass.commutes {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} :
              ∀ {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Semiring B} {inst_3 : Algebra R A} {inst_4 : Algebra R B} {inst_5 : FunLike F A B} [self : AlgHomClass F R A B] (f : F) (r : R), f ((algebraMap R A) r) = (algebraMap R B) r
              @[instance 100]
              instance AlgHomClass.linearMapClass {R : Type u_1} {A : Type u_2} {B : Type u_3} {F : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] :
              Equations
              • =
              def AlgHomClass.toAlgHom {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 : Type u_5} [FunLike F A B] [AlgHomClass F R A B] (f : F) :

              Turn an element of a type F satisfying AlgHomClass F α β into an actual AlgHom. This is declared as the default coercion from F to α →+* β.

              Equations
              • f = { toFun := f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
              Instances For
                instance AlgHomClass.coeTC {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 : Type u_5} [FunLike F A B] [AlgHomClass F R A B] :
                CoeTC F (A →ₐ[R] B)
                Equations
                • AlgHomClass.coeTC = { coe := AlgHomClass.toAlgHom }
                instance AlgHom.funLike {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                FunLike (A →ₐ[R] B) A B
                Equations
                • AlgHom.funLike = { coe := fun (f : A →ₐ[R] B) => (↑f.toRingHom).toFun, coe_injective' := }
                instance AlgHom.algHomClass {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                AlgHomClass (A →ₐ[R] B) R A B
                Equations
                • =
                def AlgHom.Simps.apply {R : Type u} {α : Type v} {β : Type w} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) :
                αβ

                See Note [custom simps projection]

                Equations
                Instances For
                  @[simp]
                  theorem AlgHom.coe_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {F : Type u_1} [FunLike F A B] [AlgHomClass F R A B] (f : F) :
                  f = f
                  @[simp]
                  theorem AlgHom.toFun_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                  (↑f.toRingHom).toFun = f
                  def AlgHom.toMonoidHom' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                  A →* B
                  Equations
                  • f = f
                  Instances For
                    instance AlgHom.coeOutMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                    CoeOut (A →ₐ[R] B) (A →* B)
                    Equations
                    • AlgHom.coeOutMonoidHom = { coe := AlgHom.toMonoidHom' }
                    def AlgHom.toAddMonoidHom' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                    A →+ B
                    Equations
                    • f = f
                    Instances For
                      instance AlgHom.coeOutAddMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                      CoeOut (A →ₐ[R] B) (A →+ B)
                      Equations
                      • AlgHom.coeOutAddMonoidHom = { coe := AlgHom.toAddMonoidHom' }
                      @[simp]
                      theorem AlgHom.coe_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : A →+* B} (h : ∀ (r : R), (↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r) :
                      { toRingHom := f, commutes' := h } = f
                      theorem AlgHom.coe_mks {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : AB} (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r) :
                      { toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f
                      @[simp]
                      theorem AlgHom.coe_ringHom_mk {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : A →+* B} (h : ∀ (r : R), (↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r) :
                      { toRingHom := f, commutes' := h } = f
                      @[simp]
                      theorem AlgHom.toRingHom_eq_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                      f.toRingHom = f
                      @[simp]
                      theorem AlgHom.coe_toRingHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                      f = f
                      @[simp]
                      theorem AlgHom.coe_toMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                      f = f
                      @[simp]
                      theorem AlgHom.coe_toAddMonoidHom {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
                      f = f
                      theorem AlgHom.coe_fn_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                      Function.Injective DFunLike.coe
                      theorem AlgHom.coe_fn_inj {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ₁ : A →ₐ[R] B} {φ₂ : A →ₐ[R] B} :
                      φ₁ = φ₂ φ₁ = φ₂
                      theorem AlgHom.coe_ringHom_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                      Function.Injective RingHomClass.toRingHom
                      theorem AlgHom.coe_monoidHom_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                      Function.Injective MonoidHomClass.toMonoidHom
                      theorem AlgHom.coe_addMonoidHom_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                      Function.Injective AddMonoidHomClass.toAddMonoidHom
                      theorem AlgHom.congr_fun {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ₁ : A →ₐ[R] B} {φ₂ : A →ₐ[R] B} (H : φ₁ = φ₂) (x : A) :
                      φ₁ x = φ₂ x
                      theorem AlgHom.congr_arg {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {x : A} {y : A} (h : x = y) :
                      φ x = φ y
                      theorem AlgHom.ext {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {φ₁ : A →ₐ[R] B} {φ₂ : A →ₐ[R] B} (H : ∀ (x : A), φ₁ x = φ₂ x) :
                      φ₁ = φ₂
                      @[simp]
                      theorem AlgHom.mk_coe {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : A →ₐ[R] B} (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r) :
                      { toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f
                      @[simp]
                      theorem AlgHom.commutes {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (r : R) :
                      φ ((algebraMap R A) r) = (algebraMap R B) r
                      theorem AlgHom.comp_algebraMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
                      (↑φ).comp (algebraMap R A) = algebraMap R B
                      @[deprecated map_add]
                      theorem AlgHom.map_add {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (r : A) (s : A) :
                      φ (r + s) = φ r + φ s
                      @[deprecated map_zero]
                      theorem AlgHom.map_zero {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
                      φ 0 = 0
                      @[deprecated map_mul]
                      theorem AlgHom.map_mul {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) (y : A) :
                      φ (x * y) = φ x * φ y
                      @[deprecated map_one]
                      theorem AlgHom.map_one {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
                      φ 1 = 1
                      @[deprecated map_pow]
                      theorem AlgHom.map_pow {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) (n : ) :
                      φ (x ^ n) = φ x ^ n
                      @[deprecated map_smul]
                      theorem AlgHom.map_smul {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (r : R) (x : A) :
                      φ (r x) = r φ x
                      @[deprecated map_sum]
                      theorem AlgHom.map_sum {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ιA) (s : Finset ι) :
                      φ (∑ xs, f x) = xs, φ (f x)
                      @[deprecated map_finsupp_sum]
                      theorem AlgHom.map_finsupp_sum {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ιαA) :
                      φ (f.sum g) = f.sum fun (i : ι) (a : α) => φ (g i a)
                      def AlgHom.mk' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), f (c x) = c f x) :

                      If a RingHom is R-linear, then it is an AlgHom.

                      Equations
                      • AlgHom.mk' f h = { toFun := f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                      Instances For
                        @[simp]
                        theorem AlgHom.coe_mk' {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →+* B) (h : ∀ (c : R) (x : A), f (c x) = c f x) :
                        (AlgHom.mk' f h) = f
                        def AlgHom.id (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

                        Identity map as an AlgHom.

                        Equations
                        Instances For
                          @[simp]
                          theorem AlgHom.coe_id (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :
                          (AlgHom.id R A) = id
                          @[simp]
                          theorem AlgHom.id_toRingHom (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :
                          theorem AlgHom.id_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (p : A) :
                          (AlgHom.id R A) p = p
                          def AlgHom.comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :

                          Composition of algebra homeomorphisms.

                          Equations
                          • φ₁.comp φ₂ = { toRingHom := φ₁.comp φ₂, commutes' := }
                          Instances For
                            @[simp]
                            theorem AlgHom.coe_comp {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
                            (φ₁.comp φ₂) = φ₁ φ₂
                            theorem AlgHom.comp_apply {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A) :
                            (φ₁.comp φ₂) p = φ₁ (φ₂ p)
                            theorem AlgHom.comp_toRingHom {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) :
                            (φ₁.comp φ₂) = (↑φ₁).comp φ₂
                            @[simp]
                            theorem AlgHom.comp_id {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
                            φ.comp (AlgHom.id R A) = φ
                            @[simp]
                            theorem AlgHom.id_comp {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
                            (AlgHom.id R B).comp φ = φ
                            theorem AlgHom.comp_assoc {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} {D : Type v₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Semiring D] [Algebra R A] [Algebra R B] [Algebra R C] [Algebra R D] (φ₁ : C →ₐ[R] D) (φ₂ : B →ₐ[R] C) (φ₃ : A →ₐ[R] B) :
                            (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
                            def AlgHom.toLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :

                            R-Alg ⥤ R-Mod

                            Equations
                            • φ.toLinearMap = { toFun := φ, map_add' := , map_smul' := }
                            Instances For
                              @[simp]
                              theorem AlgHom.toLinearMap_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (p : A) :
                              φ.toLinearMap p = φ p
                              theorem AlgHom.toLinearMap_injective {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :
                              Function.Injective AlgHom.toLinearMap
                              @[simp]
                              theorem AlgHom.comp_toLinearMap {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
                              (g.comp f).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap
                              @[simp]
                              theorem AlgHom.toLinearMap_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                              (AlgHom.id R A).toLinearMap = LinearMap.id
                              def AlgHom.ofLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) :

                              Promote a LinearMap to an AlgHom by supplying proofs about the behavior on 1 and *.

                              Equations
                              • AlgHom.ofLinearMap f map_one map_mul = { toFun := f, map_one' := map_one, map_mul' := map_mul, map_zero' := , map_add' := , commutes' := }
                              Instances For
                                @[simp]
                                theorem AlgHom.ofLinearMap_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) (a : A) :
                                (AlgHom.ofLinearMap f map_one map_mul) a = f a
                                @[simp]
                                theorem AlgHom.ofLinearMap_toLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (map_one : φ.toLinearMap 1 = 1) (map_mul : ∀ (x y : A), φ.toLinearMap (x * y) = φ.toLinearMap x * φ.toLinearMap y) :
                                AlgHom.ofLinearMap φ.toLinearMap map_one map_mul = φ
                                @[simp]
                                theorem AlgHom.toLinearMap_ofLinearMap {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) (map_one : f 1 = 1) (map_mul : ∀ (x y : A), f (x * y) = f x * f y) :
                                (AlgHom.ofLinearMap f map_one map_mul).toLinearMap = f
                                @[simp]
                                theorem AlgHom.ofLinearMap_id {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (map_one : LinearMap.id 1 = 1) (map_mul : ∀ (x y : A), LinearMap.id (x * y) = LinearMap.id x * LinearMap.id y) :
                                AlgHom.ofLinearMap LinearMap.id map_one map_mul = AlgHom.id R A
                                theorem AlgHom.map_smul_of_tower {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {R' : Type u_1} [SMul R' A] [SMul R' B] [LinearMap.CompatibleSMul A B R' R] (r : R') (x : A) :
                                φ (r x) = r φ x
                                @[deprecated map_list_prod]
                                theorem AlgHom.map_list_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : List A) :
                                φ s.prod = (List.map (⇑φ) s).prod
                                instance AlgHom.End {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                Equations
                                • AlgHom.End = Monoid.mk npowRecAuto
                                theorem AlgHom.End_toOne_one {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
                                1 = AlgHom.id R A
                                theorem AlgHom.End_toSemigroup_toMul_mul {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (φ₁ : A →ₐ[R] A) (φ₂ : A →ₐ[R] A) :
                                φ₁ * φ₂ = φ₁.comp φ₂
                                @[simp]
                                theorem AlgHom.one_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :
                                1 x = x
                                @[simp]
                                theorem AlgHom.mul_apply {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] (φ : A →ₐ[R] A) (ψ : A →ₐ[R] A) (x : A) :
                                (φ * ψ) x = φ (ψ x)
                                theorem AlgHom.algebraMap_eq_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) {y : R} {x : A} (h : (algebraMap R A) y = x) :
                                (algebraMap R B) y = f x
                                @[deprecated map_multiset_prod]
                                theorem AlgHom.map_multiset_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (s : Multiset A) :
                                φ s.prod = (Multiset.map (⇑φ) s).prod
                                @[deprecated map_prod]
                                theorem AlgHom.map_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ιA) (s : Finset ι) :
                                φ (∏ xs, f x) = xs, φ (f x)
                                @[deprecated map_finsupp_prod]
                                theorem AlgHom.map_finsupp_prod {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) {α : Type u_1} [Zero α] {ι : Type u_2} (f : ι →₀ α) (g : ιαA) :
                                φ (f.prod g) = f.prod fun (i : ι) (a : α) => φ (g i a)
                                @[deprecated map_neg]
                                theorem AlgHom.map_neg {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) :
                                φ (-x) = -φ x
                                @[deprecated map_sub]
                                theorem AlgHom.map_sub {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (x : A) (y : A) :
                                φ (x - y) = φ x - φ y
                                def RingHom.toNatAlgHom {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) :

                                Reinterpret a RingHom as an -algebra homomorphism.

                                Equations
                                • f.toNatAlgHom = { toFun := f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                                Instances For
                                  @[simp]
                                  theorem RingHom.toNatAlgHom_coe {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) :
                                  f.toNatAlgHom = f
                                  theorem RingHom.toNatAlgHom_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (x : R) :
                                  f.toNatAlgHom x = f x
                                  def RingHom.toIntAlgHom {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) :

                                  Reinterpret a RingHom as a -algebra homomorphism.

                                  Equations
                                  • f.toIntAlgHom = { toRingHom := f, commutes' := }
                                  Instances For
                                    @[simp]
                                    theorem RingHom.toIntAlgHom_coe {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) :
                                    f.toIntAlgHom = f
                                    theorem RingHom.toIntAlgHom_apply {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (x : R) :
                                    f.toIntAlgHom x = f x
                                    theorem RingHom.toIntAlgHom_injective {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] :
                                    Function.Injective RingHom.toIntAlgHom
                                    def Algebra.ofId (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

                                    AlgebraMap as an AlgHom.

                                    Equations
                                    Instances For
                                      theorem Algebra.ofId_apply {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
                                      (Algebra.ofId R A) r = (algebraMap R A) r
                                      instance Algebra.subsingleton_id {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] :

                                      This is a special case of a more general instance that we define in a later file.

                                      Equations
                                      • =
                                      theorem Algebra.ext_id {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] (f : R →ₐ[R] A) (g : R →ₐ[R] A) :
                                      f = g

                                      This ext lemma closes trivial subgoals create when chaining heterobasic ext lemmas.

                                      @[simp]
                                      theorem Algebra.smul_units_def {R : Type u} (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] (f : A →ₐ[R] A) (x : Aˣ) :
                                      f x = (Units.map f) x
                                      def MulSemiringAction.toAlgHom {M : Type u_1} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A] (m : M) :

                                      Each element of the monoid defines an algebra homomorphism.

                                      This is a stronger version of MulSemiringAction.toRingHom and DistribMulAction.toLinearMap.

                                      Equations
                                      • MulSemiringAction.toAlgHom R A m = { toFun := fun (a : A) => m a, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
                                      Instances For
                                        @[simp]
                                        theorem MulSemiringAction.toAlgHom_apply {M : Type u_1} (R : Type u_3) (A : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [MulSemiringAction M A] [SMulCommClass M R A] (m : M) (a : A) :