noncomputable def Proposition22_7.Obj : Type

noncomputable def Proposition22_7.Weight : Type

noncomputable def Proposition22_7.Funct : Type

noncomputable def Proposition22_7.FObj : Funct → Obj → Obj

noncomputable def Proposition22_7.VermaModule : Weight → Obj

noncomputable def Proposition22_7.ProjectiveCover : Weight → Obj

noncomputable def Proposition22_7.rho : Weight

noncomputable def Proposition22_7.IsProjectiveFunctor : Funct → Prop

noncomputable def Proposition22_7.IsIndecomposableObj : Obj → Prop

noncomputable def Proposition22_7.IsProjectiveObj : Obj → Prop

noncomputable def Proposition22_7.IsIndecomposable : Funct → Prop

noncomputable def Proposition22_7.IsDominant : Weight → Prop

noncomputable def Proposition22_7.FactorsThroughBlock : Funct → Weight → Prop

noncomputable def Proposition22_7.IsDirectSumDecomp (F : Funct) {n : ℕ} (F_i : Fin n → Funct) : Prop

noncomputable def Proposition22_7.IsDirectSumDecompObj (M : Obj) {n : ℕ} (summands : Fin n → Obj) : Prop

noncomputable def Proposition22_7.ObjIso : Obj → Obj → Prop

theorem Proposition22_7.krullSchmidt (M : Obj) : ∃ (n : ℕ), ∃ (summands : Fin n → Obj), IsDirectSumDecompObj M summands ∧ ∀ (i : Fin n), IsIndecomposableObj (summands i)

theorem Proposition22_7.corollary_22_6_ii (F : Funct) (hF : IsProjectiveFunctor F) (lam : Weight) (n : ℕ) (summands : Fin n → Obj) (hDecomp : IsDirectSumDecompObj (FObj F (VermaModule lam)) summands) : ∃ (F_i : Fin n → Funct), (∀ (i : Fin n), IsProjectiveFunctor (F_i i)) ∧ (∀ (i : Fin n), ObjIso (FObj (F_i i) (VermaModule lam)) (summands i)) ∧ IsDirectSumDecomp F F_i

theorem Proposition22_7.indecomposable_transfer (F_i : Funct) (hFi : IsProjectiveFunctor F_i) (lam : Weight) (hEval : IsIndecomposableObj (FObj F_i (VermaModule lam))) : IsIndecomposable F_i

theorem Proposition22_7.projective_functor_preserves_proj (F : Funct) (hF : IsProjectiveFunctor F) (M : Obj) (hM : IsProjectiveObj M) : IsProjectiveObj (FObj F M)

theorem Proposition22_7.verma_projective_of_dominant (lam : Weight) (hDom : IsDominant lam) : IsProjectiveObj (VermaModule lam)

theorem Proposition22_7.functor_indecomp_implies_module_indecomp (F : Funct) (hF : IsProjectiveFunctor F) (hIndecomp : IsIndecomposable F) (lam : Weight) : IsIndecomposableObj (FObj F (VermaModule lam))

theorem Proposition22_7.indecomposable_projective_is_cover (M : Obj) (hIndecomp : IsIndecomposableObj M) (hProj : IsProjectiveObj M) : ∃ (mu : Weight), ObjIso M (ProjectiveCover mu)

theorem Proposition22_7.indecomp_of_iso (M N : Obj) (h : ObjIso M N) (hN : IsIndecomposableObj N) : IsIndecomposableObj M

theorem Proposition22_7.proposition_22_7_i (F : Funct) (hF : IsProjectiveFunctor F) (lam : Weight) : ∃ (n : ℕ), ∃ (F_i : Fin n → Funct), (∀ (i : Fin n), IsProjectiveFunctor (F_i i)) ∧ (∀ (i : Fin n), IsIndecomposable (F_i i)) ∧ IsDirectSumDecomp F F_i

theorem Proposition22_7.proposition_22_7_ii (F : Funct) (hF : IsProjectiveFunctor F) (hIndecomp : IsIndecomposable F) (lam : Weight) (hDom : IsDominant lam) (hBlock : FactorsThroughBlock F lam) : ∃ (mu : Weight), ObjIso (FObj F (VermaModule lam)) (ProjectiveCover mu)