Theorems · Definition · commutative algebra

GradedRingHom.ofClass

{ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] →
                [inst_3 : SetLike τ B] →
                  {𝒜 : ι → σ} →
                    {ℬ : ι → τ} →
                      {F : Type u_10} →
                        [inst_4 : FunLike F A B] → [GradedFunLike F 𝒜 ℬ] → [RingHomClass F A B] → F → 𝒜 →+*ᵍ ℬ

Turn an element of a type F satisfying [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B] into an actual GradedRingHom. This should not be used directly. In the future, Mathlib will prefer structural projections over these general constructions from hom classes.

Defined in

Mathlib.RingTheory.GradedAlgebra.RingHom

Cited by

5 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

SemiringSemiringSetLikeSetLikeFunLikeGradedFunLikeRingHomClass