theorem IsCategoryO_of_lieEquiv {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {A : Type u_3} [AddCommGroup A] [Module R A] [LieRingModule 𝔤 A] [LieModule R 𝔤 A] {B : Type u_4} [AddCommGroup B] [Module R B] [LieRingModule 𝔤 B] [LieModule R 𝔤 B] (f : A ≃ₗ⁅R,𝔤⁆ B) (hB : IsCategoryO Δ rd B) : IsCategoryO Δ rd A

theorem tensorProduct_isCategoryO_aux {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {V : Type u_3} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] {M : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) : IsCategoryO Δ rd (TensorProduct R V M)

theorem tensor_finiteDim_categoryO {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {V : Type u_3} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] {M : Type u_4} [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (hM : IsCategoryO Δ rd M) {VM : Type u_5} [AddCommGroup VM] [Module R VM] [LieRingModule 𝔤 VM] [LieModule R 𝔤 VM] (tensor_iso : VM ≃ₗ⁅R,𝔤⁆ TensorProduct R V M) : IsCategoryO Δ rd VM

structure HasVermaFiltration {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (Δ_weights : Multiset (↥Δ.𝔥 →ₗ[R] R)) : Type (max (max u_1 u_2) u_3)

• length : ℕ
• filtration : Fin (self.length + 1) → LieSubmodule R 𝔤 M
• mono (i : Fin self.length) : self.filtration ⟨↑i, ⋯⟩ ≤ self.filtration ⟨↑i + 1, ⋯⟩
• bot : self.filtration ⟨0, ⋯⟩ = ⊥
• top : self.filtration ⟨self.length, ⋯⟩ = ⊤
• quotient_weights : Fin self.length → ↥Δ.𝔥 →ₗ[R] R
• weights_eq : Multiset.map self.quotient_weights Finset.univ.val = Δ_weights
• quotient_is_verma (i : Fin self.length) : ∃ (Q : Type u_4) (x : AddCommGroup Q) (x_1 : Module R Q) (x_2 : LieRingModule 𝔤 Q) (x_3 : LieModule R 𝔤 Q), Nonempty (IsVermaModule Δ Q (self.quotient_weights i))

theorem verma_tensor_finiteDim_filtration {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {Mlam : Type u_3} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (lam : ↥Δ.𝔥 →ₗ[R] R) (hMlam : IsVermaModule Δ Mlam lam) {V : Type u_4} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] {T : Type u_5} [AddCommGroup T] [Module R T] [LieRingModule 𝔤 T] [LieModule R 𝔤 T] (tensor_iso : T ≃ₗ⁅R,𝔤⁆ TensorProduct R Mlam V) : ∃ (Δ_weights : Multiset (↥Δ.𝔥 →ₗ[R] R)) (filt : HasVermaFiltration T Δ_weights), filt.length = Module.finrank R V ∧ ∀ (i : Fin filt.length), ∃ (μ : ↥Δ.𝔥 →ₗ[R] R), filt.quotient_weights i = lam + μ

theorem tensor_verma_projective_of_dominant {R : Type v} [Field R] {𝔤 : Type v} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wg : WeylGroupData Δ} {Mlam : Type v} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (lam : ↥Δ.𝔥 →ₗ[R] R) (hdom : IsDominantWeightLE rd wg lam) (hMlam : IsVermaModule Δ Mlam (lam - wg.ρ)) (hMlamO : IsCategoryO Δ rd Mlam) {V : Type v} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] [Module.Free R V] {VP : Type v} [AddCommGroup VP] [Module R VP] [LieRingModule 𝔤 VP] [LieModule R 𝔤 VP] (hVPO : IsCategoryO Δ rd VP) (tensor_iso : VP ≃ₗ⁅R,𝔤⁆ TensorProduct R V Mlam) : IsProjectiveInO rd VP hVPO

structure CategoryOProperties {R : Type u_1} [Field R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) : Prop

• noetherian (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] : IsCategoryO Δ rd M → ∀ (chain : ℕ → LieSubmodule R 𝔤 M), (∀ (n : ℕ), chain n ≤ chain (n + 1)) → ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → chain n = chain N
• enough_projectives (M : Type u_4) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] : IsCategoryO Δ rd M → ∃ (P : Type u_5) (x : AddCommGroup P) (x_1 : Module R P) (x_2 : LieRingModule 𝔤 P) (x_3 : LieModule R 𝔤 P) (hPO : IsCategoryO Δ rd P), IsProjectiveInO rd P hPO ∧ ∃ (f : P →ₗ⁅R,𝔤⁆ M), Function.Surjective ⇑f
• hom_finiteDimensional (P : Type u_6) [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) : IsProjectiveInO rd P hPO → ∀ (M : Type u_7) [inst : AddCommGroup M] [inst✝ : Module R M] [inst✝¹ : LieRingModule 𝔤 M] [inst✝² : LieModule R 𝔤 M], IsCategoryO Δ rd M → Module.Finite R (P →ₗ⁅R,𝔤⁆ M)