Documentation

Mathlib.Algebra.Homology.ShortComplex.Linear

Homology of linear categories #

In this file, it is shown that if C is a R-linear category, then ShortComplex C is a R-linear category. Various homological notions are also shown to be linear.

source
instance CategoryTheory.ShortComplex.instSMulHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplex {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} :
SMul R (S₁ ⟶ S₂)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.ShortComplex.smul_τ₁ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (a : R) (φ : S₁ ⟶ S₂) :
(a • φ).τ₁ = a • φ.τ₁
source
@[simp]
theorem CategoryTheory.ShortComplex.smul_τ₂ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (a : R) (φ : S₁ ⟶ S₂) :
(a • φ).τ₂ = a • φ.τ₂
source
@[simp]
theorem CategoryTheory.ShortComplex.smul_τ₃ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (a : R) (φ : S₁ ⟶ S₂) :
(a • φ).τ₃ = a • φ.τ₃
source
instance CategoryTheory.ShortComplex.instModuleHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplexToAddCommMonoidInstAddCommGroupHomShortComplexPreadditiveHasZeroMorphismsToQuiverToCategoryStructInstCategoryShortComplex {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} :
Module R (S₁ ⟶ S₂)
Equations
  • One or more equations did not get rendered due to their size.
source
instance CategoryTheory.ShortComplex.instLinearShortComplexPreadditiveHasZeroMorphismsInstCategoryShortComplexInstPreadditiveShortComplexPreadditiveHasZeroMorphismsInstCategoryShortComplex {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] :
CategoryTheory.Linear R (CategoryTheory.ShortComplex C)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (a : R) :
(CategoryTheory.ShortComplex.LeftHomologyMapData.smul γ a).φK = a • γ.φK
source
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (a : R) :
(CategoryTheory.ShortComplex.LeftHomologyMapData.smul γ a).φH = a • γ.φH
source
def CategoryTheory.ShortComplex.LeftHomologyMapData.smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (a : R) :
CategoryTheory.ShortComplex.LeftHomologyMapData (a • φ) h₁ h₂

Given a left homology map data for morphism φ, this is the induced left homology map data for a • φ.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.leftHomologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) (a : R) :
    CategoryTheory.ShortComplex.leftHomologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.cyclesMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.LeftHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.LeftHomologyData S₂) (a : R) :
    CategoryTheory.ShortComplex.cyclesMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.cyclesMap' φ h₁ h₂
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.leftHomologyMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :
    CategoryTheory.ShortComplex.leftHomologyMap (a • φ) = a • CategoryTheory.ShortComplex.leftHomologyMap φ
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.cyclesMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [CategoryTheory.ShortComplex.HasLeftHomology S₁] [CategoryTheory.ShortComplex.HasLeftHomology S₂] :
    CategoryTheory.ShortComplex.cyclesMap (a • φ) = a • CategoryTheory.ShortComplex.cyclesMap φ
    source
    instance CategoryTheory.ShortComplex.leftHomologyFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] :
    CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.leftHomologyFunctor C)
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.ShortComplex.cyclesFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] :
    CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.cyclesFunctor C)
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (a : R) :
    (CategoryTheory.ShortComplex.RightHomologyMapData.smul γ a).φQ = a • γ.φQ
    source
    @[simp]
    theorem CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (a : R) :
    (CategoryTheory.ShortComplex.RightHomologyMapData.smul γ a).φH = a • γ.φH
    source
    def CategoryTheory.ShortComplex.RightHomologyMapData.smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁} {h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (a : R) :
    CategoryTheory.ShortComplex.RightHomologyMapData (a • φ) h₁ h₂

    Given a right homology map data for morphism φ, this is the induced right homology map data for a • φ.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.rightHomologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (a : R) :
      CategoryTheory.ShortComplex.rightHomologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.opcyclesMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ShortComplex.RightHomologyData S₁) (h₂ : CategoryTheory.ShortComplex.RightHomologyData S₂) (a : R) :
      CategoryTheory.ShortComplex.opcyclesMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.rightHomologyMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] :
      CategoryTheory.ShortComplex.rightHomologyMap (a • φ) = a • CategoryTheory.ShortComplex.rightHomologyMap φ
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.opcyclesMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [CategoryTheory.ShortComplex.HasRightHomology S₁] [CategoryTheory.ShortComplex.HasRightHomology S₂] :
      CategoryTheory.ShortComplex.opcyclesMap (a • φ) = a • CategoryTheory.ShortComplex.opcyclesMap φ
      source
      instance CategoryTheory.ShortComplex.rightHomologyFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] :
      CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.rightHomologyFunctor C)
      Equations
      • ⋯ = ⋯
      source
      instance CategoryTheory.ShortComplex.opcyclesFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] :
      CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.opcyclesFunctor C)
      Equations
      • ⋯ = ⋯
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.HomologyMapData.smul_right {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (a : R) :
      (CategoryTheory.ShortComplex.HomologyMapData.smul γ a).right = CategoryTheory.ShortComplex.RightHomologyMapData.smul γ.right a
      source
      @[simp]
      theorem CategoryTheory.ShortComplex.HomologyMapData.smul_left {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (a : R) :
      (CategoryTheory.ShortComplex.HomologyMapData.smul γ a).left = CategoryTheory.ShortComplex.LeftHomologyMapData.smul γ.left a
      source
      def CategoryTheory.ShortComplex.HomologyMapData.smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : CategoryTheory.ShortComplex.HomologyData S₁} {h₂ : CategoryTheory.ShortComplex.HomologyData S₂} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (a : R) :
      CategoryTheory.ShortComplex.HomologyMapData (a • φ) h₁ h₂

      Given a homology map data for a morphism φ, this is the induced homology map data for a • φ.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.homologyMap'_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} (h₁ : CategoryTheory.ShortComplex.HomologyData S₁) (h₂ : CategoryTheory.ShortComplex.HomologyData S₂) (a : R) :
        CategoryTheory.ShortComplex.homologyMap' (a • φ) h₁ h₂ = a • CategoryTheory.ShortComplex.homologyMap' φ h₁ h₂
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.homologyMap_smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (a : R) [CategoryTheory.ShortComplex.HasHomology S₁] [CategoryTheory.ShortComplex.HasHomology S₂] :
        CategoryTheory.ShortComplex.homologyMap (a • φ) = a • CategoryTheory.ShortComplex.homologyMap φ
        source
        instance CategoryTheory.ShortComplex.homologyFunctor_linear {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] [CategoryTheory.CategoryWithHomology C] :
        CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.homologyFunctor C)
        Equations
        • ⋯ = ⋯
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₀ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (CategoryTheory.ShortComplex.Homotopy.smul h a).h₀ = a • h.h₀
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₃ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (CategoryTheory.ShortComplex.Homotopy.smul h a).h₃ = a • h.h₃
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₁ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (CategoryTheory.ShortComplex.Homotopy.smul h a).h₁ = a • h.h₁
        source
        @[simp]
        theorem CategoryTheory.ShortComplex.Homotopy.smul_h₂ {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        (CategoryTheory.ShortComplex.Homotopy.smul h a).h₂ = a • h.h₂
        source
        def CategoryTheory.ShortComplex.Homotopy.smul {R : Type u_1} {C : Type u_2} [Semiring R] [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ ⟶ S₂} {φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R) :
        CategoryTheory.ShortComplex.Homotopy (a • φ₁) (a • φ₂)

        Homotopy between morphisms of short complexes is compatible with the scalar multiplication.

        Equations
        Instances For