def IsInjectiveInO {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (I : Type uCatO) [AddCommGroup I] [Module R I] [LieRingModule 𝔤 I] [LieModule R 𝔤 I] (_hI : IsCategoryO Δ rd I) : Prop

theorem duality_projective_to_injective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {P : Type uCatO} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (dP : DualInO cτ P hPO) : IsInjectiveInO rd dP.Xdual ⋯

theorem injective_hull_simple_is_dual_projective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {_wg : WeylGroupData Δ} (cτ : CartanInvolution rd) (lam : ↥Δ.𝔥 →ₗ[R] R) {Llam : Type uCatO} [AddCommGroup Llam] [Module R Llam] [LieRingModule 𝔤 Llam] [LieModule R 𝔤 Llam] (hLO : IsCategoryO Δ rd Llam) (hLirr : LieModule.IsIrreducible R 𝔤 Llam) (hLhw : IsHighestWeightModule Δ Llam lam) {Plam : Type uCatO} [AddCommGroup Plam] [Module R Plam] [LieRingModule 𝔤 Plam] [LieModule R 𝔤 Plam] (hPO : IsCategoryO Δ rd Plam) (hPproj : IsProjectiveInO rd Plam hPO) (hPsurj : ∃ (π : Plam →ₗ⁅R,𝔤⁆ Llam), Function.Surjective ⇑π) (dP : DualInO cτ Plam hPO) : IsInjectiveInO rd dP.Xdual ⋯ ∧ ∃ (ι : Llam →ₗ⁅R,𝔤⁆ dP.Xdual), Function.Injective ⇑ι ∧ ∀ (N : LieSubmodule R 𝔤 dP.Xdual), N ≠ ⊥ → ∃ (v : Llam), v ≠ 0 ∧ ι v ∈ N