Mathlib Map

Structures Β· Data types

GradedFunLike

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
Shape
3 explicit arguments Β· adds map_mem
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances2

  • GradedAlgHom
  • GradedRingHom

How is a type an instance?

Loading the hierarchy index…

Assumed by12

Ancestors0

No ancestors.