Theorems · Definition · ring theory

GradedAlgHom.toEnd

{R : Type u_1} →
  {A : Type u_6} →
    {ι : Type u_10} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : DecidableEq ι] →
              [inst_4 : AddMonoid ι] → {𝒜 : ι → Submodule R A} → [inst_5 : GradedAlgebra 𝒜] → (𝒜 →ₐᵍ[R] 𝒜) →* A →ₐ[R] A

We enrich the existing function toAlgHom with the structure of a MonoidHom, to produce a bundled function that we now call toEnd.

Defined in

Mathlib.RingTheory.GradedAlgebra.AlgHom

Cited by

1 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebraDecidableEqAddMonoidGradedAlgebra