Theorems · Inductive type · ring theory

GradedFunLike

(F : Type u_1) →
  {A : outParam (Type u_2)} →
    {B : outParam (Type u_3)} →
      {σ : outParam (Type u_4)} →
        {τ : outParam (Type u_5)} →
          {ι : outParam (Type u_6)} →
            [SetLike σ A] → [SetLike τ B] → outParam (ι → σ) → outParam (ι → τ) → [FunLike F A B] → Prop

The class GradedFunLike F 𝒜 ℬ expresses that terms of type F have an injective coercion to grading-preserving functions from A to B, where 𝒜 is a grading on A and ℬ is a grading on B. This typeclass has [FunLike F A B] as one of the assumptions. This typeclass is used in the characterisation of certain types of graded homomorphisms, such as GradedRingHom and GradedAlgHom. For example, what would be called "GradedRingHomClass F 𝒜 ℬ" would be expressed as [FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B].

Defined in

Mathlib.Data.FunLike.Graded

Cited by

9 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

SetLikeSetLikeFunLike