Documentation

Mathlib.Data.FunLike.Graded

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.

source
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 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].

  • map_mem (f : F) {i : ΞΉ} {x : A} : x ∈ π’œ i β†’ f x ∈ ℬ i
Instances
    source
    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
    source
    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
    Instances For
      source
      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.

      Instances
        source
        @[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 π’œ ℬ
        source
        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
        source
        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.

        source
        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.

        source
        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
        Instances For
          source
          @[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
          source
          @[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