Class of grading-preserving functions

We define GradedFunLike F 𝒜 ℬ where 𝒜 and ℬ represent some sort of grading. This class assumes FunLike A B where A and B are the underlying types.

class 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 charactersation 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].

• map_mem (f : F) {i : ι} {x : A} : x ∈ 𝒜 i → f x ∈ ℬ i

theorem map_mem {F : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] (f : F) {i : ι} {x : A} (h : x ∈ 𝒜 i) : f x ∈ ℬ i

def mapGraded {F : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [FunLike F A B] [GradedFunLike F 𝒜 ℬ] (f : F) (i : ι) (x : ↥(𝒜 i)) : ↥(ℬ i)

A graded map descends to a map on each component.

Equations

• mapGraded f i x = ⟨f ↑x, ⋯⟩