structure CartanInvolution {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) : Type u_2

• τ : 𝔤 →ₗ[R] 𝔤
• involution : self.τ ∘ₗ self.τ = LinearMap.id
• negate_cartan (h : ↥Δ.𝔥) : self.τ ↑h = -↑h
• anti_hom (X Y : 𝔤) : self.τ ⁅X, Y⁆ = ⁅self.τ Y, self.τ X⁆

structure DualInO {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) (X : Type uCatO) [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : IsCategoryO Δ rd X) : Type (max (max (uCatO + 1) u_1) u_2)

• Xdual : Type uCatO
• instAddCommGroup : AddCommGroup self.Xdual
• instModule : Module R self.Xdual
• instLieRingModule : LieRingModule 𝔤 self.Xdual
• instLieModule : LieModule R 𝔤 self.Xdual
• isCategoryO : IsCategoryO Δ rd self.Xdual

def dualInO {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : IsCategoryO Δ rd X) : DualInO cτ X hX

theorem prop_20_9_ii_simple_self_dual {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {Llam : Type uCatO} [AddCommGroup Llam] [Module R Llam] [LieRingModule 𝔤 Llam] [LieModule R 𝔤 Llam] (lam : ↥Δ.𝔥 →ₗ[R] R) (hLO : IsCategoryO Δ rd Llam) (hLirr : LieModule.IsIrreducible R 𝔤 Llam) (hLhw : IsHighestWeightModule Δ Llam lam) (d : DualInO cτ Llam hLO) : LieModule.IsIrreducible R 𝔤 d.Xdual ∧ Nonempty (IsHighestWeightModule Δ d.Xdual lam) ∧ ∃ (iso : Llam →ₗ⁅R,𝔤⁆ d.Xdual), Function.Bijective ⇑iso

def IsContragredientVerma {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (M : Type uCatO) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (lam : ↥Δ.𝔥 →ₗ[R] R) (_hM : IsCategoryO Δ rd M) : Prop

theorem prop_20_9_ii_verma_dual_contragredient {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {Mlam : Type uCatO} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (lam : ↥Δ.𝔥 →ₗ[R] R) (hMlam : IsVermaModule Δ Mlam lam) (hMlamO : IsCategoryO Δ rd Mlam) (d : DualInO cτ Mlam hMlamO) : IsContragredientVerma rd d.Xdual lam ⋯

theorem prop_20_9_iii_contravariant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : IsCategoryO Δ rd X) {Y : Type uCatO} [AddCommGroup Y] [Module R Y] [LieRingModule 𝔤 Y] [LieModule R 𝔤 Y] (hY : IsCategoryO Δ rd Y) (f : X →ₗ⁅R,𝔤⁆ Y) (dX : DualInO cτ X hX) (dY : DualInO cτ Y hY) : ∃ (fdual : dY.Xdual →ₗ⁅R,𝔤⁆ dX.Xdual), (Function.Surjective ⇑f → Function.Injective ⇑fdual) ∧ (Function.Injective ⇑f → Function.Surjective ⇑fdual)

theorem prop_20_9_iii_involutive {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : IsCategoryO Δ rd X) (dX : DualInO cτ X hX) (dXdd : DualInO cτ dX.Xdual ⋯) : ∃ (iso : X →ₗ⁅R,𝔤⁆ dXdd.Xdual), Function.Bijective ⇑iso

theorem prop_20_9_iii_preserves_blocks {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) (wg : WeylGroupData Δ) {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : IsCategoryO Δ rd X) (lam : ↥Δ.𝔥 →ₗ[R] R) (hBlock : IsInBlockO Δ rd wg X lam) (d : DualInO cτ X hX) : IsInBlockO Δ rd wg d.Xdual lam

theorem simple_module_self_dual {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {Llam : Type uCatO} [AddCommGroup Llam] [Module R Llam] [LieRingModule 𝔤 Llam] [LieModule R 𝔤 Llam] (lam : ↥Δ.𝔥 →ₗ[R] R) (hLO : IsCategoryO Δ rd Llam) (hLirr : LieModule.IsIrreducible R 𝔤 Llam) (hLhw : IsHighestWeightModule Δ Llam lam) (d : DualInO cτ Llam hLO) : LieModule.IsIrreducible R 𝔤 d.Xdual ∧ Nonempty (IsHighestWeightModule Δ d.Xdual lam) ∧ ∃ (iso : Llam →ₗ⁅R,𝔤⁆ d.Xdual), Function.Bijective ⇑iso

theorem verma_dual_is_contragredient {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {Mlam : Type uCatO} [AddCommGroup Mlam] [Module R Mlam] [LieRingModule 𝔤 Mlam] [LieModule R 𝔤 Mlam] (lam : ↥Δ.𝔥 →ₗ[R] R) (hMlam : IsVermaModule Δ Mlam lam) (hMlamO : IsCategoryO Δ rd Mlam) (d : DualInO cτ Mlam hMlamO) : IsContragredientVerma rd d.Xdual lam ⋯

theorem duality_functor_contravariant {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : IsCategoryO Δ rd X) {Y : Type uCatO} [AddCommGroup Y] [Module R Y] [LieRingModule 𝔤 Y] [LieModule R 𝔤 Y] (hY : IsCategoryO Δ rd Y) (f : X →ₗ⁅R,𝔤⁆ Y) (dX : DualInO cτ X hX) (dY : DualInO cτ Y hY) : ∃ (fdual : dY.Xdual →ₗ⁅R,𝔤⁆ dX.Xdual), (Function.Surjective ⇑f → Function.Injective ⇑fdual) ∧ (Function.Injective ⇑f → Function.Surjective ⇑fdual)

theorem duality_functor_involutive {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} (cτ : CartanInvolution rd) {X : Type uCatO} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : IsCategoryO Δ rd X) (dX : DualInO cτ X hX) (dXdd : DualInO cτ dX.Xdual ⋯) : ∃ (iso : X →ₗ⁅R,𝔤⁆ dXdd.Xdual), Function.Bijective ⇑iso