Class of grading-preserving functions and isomorphisms

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.

We also define GradedEquivLike E 𝒜 ℬ, which is similar to EquivLike, where here e : E is required to satisfy x ∈ 𝒜 i ↔ e x ∈ ℬ i.

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 Graded.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 Graded.subtypeMap {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

• Graded.subtypeMap f i x = ⟨f ↑x, ⋯⟩

class GradedEquivLike (E : 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 (ι → τ)) [EquivLike E A B] : Prop

The class GradedEquivLike E 𝒜 ℬ says that E is a type of grading-preserving isomorphisms between 𝒜 and ℬ. It is the combination of GradedFunLike E 𝒜 ℬ and EquivLike E A B.

• map_mem_iff (e : E) {i : ι} {x : A} : e x ∈ ℬ i ↔ x ∈ 𝒜 i

@[instance 100]

instance GradedEquivLike.toGradedFunLike (E : Type u_1) {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] : GradedFunLike E 𝒜 ℬ

theorem Graded.map_mem_iff {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) {i : ι} {x : A} : e x ∈ ℬ i ↔ x ∈ 𝒜 i

theorem Graded.mem_of_map_mem {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) {i : ι} {x : A} : e x ∈ ℬ i → x ∈ 𝒜 i

Alias of the forward direction of Graded.map_mem_iff.

theorem Graded.map_mem_of_mem {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) {i : ι} {x : A} : x ∈ 𝒜 i → e x ∈ ℬ i

Alias of the reverse direction of Graded.map_mem_iff.

def Graded.equiv {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) (i : ι) : ↥(𝒜 i) ≃ ↥(ℬ i)

A graded isomorphism descends to an isomorphism on each component.

Equations

• Graded.equiv e i = { toFun := Graded.subtypeMap e i, invFun := fun (y : ↥(ℬ i)) => ⟨EquivLike.inv e ↑y, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Graded.equiv_symm_apply_coe {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) (i : ι) (y : ↥(ℬ i)) : ↑((equiv e i).symm y) = EquivLike.inv e ↑y

@[simp]

theorem Graded.equiv_apply {E : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} {ι : Type u_6} [SetLike σ A] [SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} [EquivLike E A B] [GradedEquivLike E 𝒜 ℬ] (e : E) (i : ι) (x : ↥(𝒜 i)) : (equiv e i) x = subtypeMap e i x