theorem
CategoryO.ext_vanishing_kernel_zero_and_iso
{R : Type u_1}
[Field R]
{𝔤 : Type u_2}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
(ci : CartanInvolution rd)
{wg : WeylGroupData Δ}
{E : Type uCatO}
[AddCommGroup E]
[Module R E]
[LieRingModule 𝔤 E]
[LieModule R 𝔤 E]
[Module.Finite R E]
[LieModule.IsTrivial 𝔤 E]
{Mlam : Type uCatO}
[AddCommGroup Mlam]
[Module R Mlam]
[LieRingModule 𝔤 Mlam]
[LieModule R 𝔤 Mlam]
(hMlamO : IsCategoryO Δ rd Mlam)
(lam : ↥Δ.𝔥 →ₗ[R] R)
(hMlam_verma : IsVermaModule Δ Mlam lam)
{K : Type uCatO}
[AddCommGroup K]
[Module R K]
[LieRingModule 𝔤 K]
[LieModule R 𝔤 K]
(hKO : IsCategoryO Δ rd K)
{Z : Type uCatO}
[AddCommGroup Z]
[Module R Z]
[LieRingModule 𝔤 Z]
[LieModule R 𝔤 Z]
(hZO : IsCategoryO Δ rd Z)
(i : K →ₗ⁅R,𝔤⁆ TensorProduct R E Mlam)
(hi : Function.Injective ⇑i)
(p : TensorProduct R E Mlam →ₗ⁅R,𝔤⁆ Z)
(hp : Function.Surjective ⇑p)
(hexact : ∀ (m : TensorProduct R E Mlam), p m = 0 ↔ ∃ (k : K), i k = m)
(hK_lam : WeightSpace Δ K lam = ⊥)
(hExtZ :
∀ (mu : ↥Δ.𝔥 →ₗ[R] R) (MmuDual : Type uCatO) [inst : AddCommGroup MmuDual] [inst_1 : Module R MmuDual]
[inst_2 : LieRingModule 𝔤 MmuDual] [inst_3 : LieModule R 𝔤 MmuDual] (hMmuDualO : IsCategoryO Δ rd MmuDual),
IsContragredientVerma rd MmuDual mu hMmuDualO →
∀ (E' : Type uCatO) [inst_4 : AddCommGroup E'] [inst_5 : Module R E'] [inst_6 : LieRingModule 𝔤 E']
[inst_7 : LieModule R 𝔤 E'],
IsCategoryO Δ rd E' →
∀ (j : MmuDual →ₗ⁅R,𝔤⁆ E'),
Function.Injective ⇑j →
∀ (q : E' →ₗ⁅R,𝔤⁆ Z), Function.Surjective ⇑q → ∃ (s : Z →ₗ⁅R,𝔤⁆ E'), ∀ (z : Z), q (s z) = z)
: