structure ProjectiveFunctors.RepGfObj (R : Type u) [CommRing R] (𝔤 : Type u) [LieRing 𝔤] [LieAlgebra R 𝔤] : Type (u + 1)

• carrier : Type u
• inst_addCommGroup : AddCommGroup self.carrier
• inst_module : Module R self.carrier
• inst_lieRingModule : LieRingModule 𝔤 self.carrier
• inst_lieModule : LieModule R 𝔤 self.carrier

opaque ProjectiveFunctors.IsLocallyFiniteCenterAction {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (_M : RepGfObj R 𝔤) : Prop

structure ProjectiveFunctors.RepGfHom {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (M N : RepGfObj R 𝔤) : Type u

• toFun : M.carrier →ₗ⁅R,𝔤⁆ N.carrier

def ProjectiveFunctors.RepGfHom.comp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {M N P : RepGfObj R 𝔤} (g : RepGfHom N P) (f : RepGfHom M N) : RepGfHom M P

def ProjectiveFunctors.RepGfHom.id {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : RepGfObj R 𝔤) : RepGfHom M M

def ProjectiveFunctors.RepGfHom.EqAsMap {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {M N : RepGfObj R 𝔤} (f g : RepGfHom M N) : Prop

opaque ProjectiveFunctors.centerActsNilpotentlyShifted_of_order {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) : Prop

theorem ProjectiveFunctors.centerActsNilpotentlyShifted_of_order_mono {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) : centerActsNilpotentlyShifted_of_order Δ M theta n → centerActsNilpotentlyShifted_of_order Δ M theta (n + 1)

theorem ProjectiveFunctors.filtration_one_step {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (M : RepGfObj R 𝔤) (n : ℕ) (_hn : centerActsNilpotentlyShifted_of_order Δ M theta (n + 2)) : ∃ (Q : RepGfObj R 𝔤) (_ : centerActsNilpotentlyShifted_of_order Δ Q theta 1) (K : RepGfObj R 𝔤) (_ : centerActsNilpotentlyShifted_of_order Δ K theta (n + 1)) (fQ : RepGfHom Q M) (fK : RepGfHom K M), ∀ (m : M.carrier), ∃ (q : Q.carrier) (k : K.carrier), fQ.toFun q + fK.toFun k = m

theorem ProjectiveFunctors.repGfObj_directSum_data {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (N₁ N₂ : RepGfObj R 𝔤) (hN₁ : centerActsNilpotentlyShifted_of_order Δ N₁ theta 1) (hN₂ : centerActsNilpotentlyShifted_of_order Δ N₂ theta 1) (M : RepGfObj R 𝔤) (f₁ : RepGfHom N₁ M) (f₂ : RepGfHom N₂ M) : ∃ (N : RepGfObj R 𝔤) (_ : centerActsNilpotentlyShifted_of_order Δ N theta 1) (f : RepGfHom N M), ∀ (m : M.carrier), (∃ (x₁ : N₁.carrier) (x₂ : N₂.carrier), f₁.toFun x₁ + f₂.toFun x₂ = m) → ∃ (y : N.carrier), f.toFun y = m

theorem ProjectiveFunctors.filtration_surjection_from_nilpotent_order {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (M : RepGfObj R 𝔤) (n : ℕ) (_hn : centerActsNilpotentlyShifted_of_order Δ M theta n) : ∃ (N : RepGfObj R 𝔤) (_ : centerActsNilpotentlyShifted_of_order Δ N theta 1) (f : RepGfHom N M), Function.Surjective ⇑f.toFun

def ProjectiveFunctors.centerActsByScalar_prop {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) : Prop

def ProjectiveFunctors.centerActsNilpotentlyShifted_prop {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem ProjectiveFunctors.centerActsByScalar_implies_nilpotentlyShifted {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) : centerActsByScalar_prop Δ M theta → centerActsNilpotentlyShifted_prop Δ M theta

structure ProjectiveFunctors.HasInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) : Prop

• center_acts_by_scalar : centerActsByScalar_prop Δ M theta

structure ProjectiveFunctors.HasGenInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) : Prop

• center_acts_nilpotently_shifted : centerActsNilpotentlyShifted_prop Δ M theta

theorem ProjectiveFunctors.hasInfChar_implies_hasGenInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : RepGfObj R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) (h : HasInfChar M theta) : HasGenInfChar M theta

structure ProjectiveFunctors.EndoFunctorData (R : Type u) [CommRing R] (𝔤 : Type u) [LieRing 𝔤] [LieAlgebra R 𝔤] : Type (u + 1)

• obj : RepGfObj R 𝔤 → RepGfObj R 𝔤
• mapHom {M N : RepGfObj R 𝔤} : RepGfHom M N → RepGfHom (self.obj M) (self.obj N)
• map_id (M : RepGfObj R 𝔤) : (self.mapHom (RepGfHom.id M)).EqAsMap (RepGfHom.id (self.obj M))
• map_comp {M N P : RepGfObj R 𝔤} (f : RepGfHom M N) (g : RepGfHom N P) : (self.mapHom (g.comp f)).EqAsMap ((self.mapHom g).comp (self.mapHom f))

structure ProjectiveFunctors.NatTransData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F G : EndoFunctorData R 𝔤) : Type (u + 1)

• app (M : RepGfObj R 𝔤) : RepGfHom (F.obj M) (G.obj M)
• naturality {M₁ M₂ : RepGfObj R 𝔤} (f : RepGfHom M₁ M₂) : ((self.app M₂).comp (F.mapHom f)).EqAsMap ((G.mapHom f).comp (self.app M₁))

def ProjectiveFunctors.NatTransData.comp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {F G H : EndoFunctorData R 𝔤} (β : NatTransData G H) (α : NatTransData F G) : NatTransData F H

def ProjectiveFunctors.NatTransData.id {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) : NatTransData F F

def ProjectiveFunctors.NatTransData.EqPointwise {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {F G : EndoFunctorData R 𝔤} (α β : NatTransData F G) : Prop

def ProjectiveFunctors.AreNatIso {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F G : EndoFunctorData R 𝔤) : Prop

def ProjectiveFunctors.IsDirectSummand {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F G : EndoFunctorData R 𝔤) : Prop

theorem ProjectiveFunctors.isDirectSummand_refl {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) : IsDirectSummand F F

def ProjectiveFunctors.IsExactSequence {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {M₁ M₂ M₃ : RepGfObj R 𝔤} (f : RepGfHom M₁ M₂) (g : RepGfHom M₂ M₃) : Prop

def ProjectiveFunctors.IsProjectiveModule {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : RepGfObj R 𝔤) : Prop

structure ProjectiveFunctors.TensorFunctorData (R : Type u) [CommRing R] (𝔤 : Type u) [LieRing 𝔤] [LieAlgebra R 𝔤] : Type (u + 1)

• V : Type u
• inst_addCommGroupV : AddCommGroup self.V
• inst_moduleV : Module R self.V
• inst_lieRingModuleV : LieRingModule 𝔤 self.V
• inst_lieModuleV : LieModule R 𝔤 self.V
• inst_finiteDimV : Module.Finite R self.V
• inst_freeV : Module.Free R self.V
• functor : EndoFunctorData R 𝔤
• tensor_obj_spec (M : RepGfObj R 𝔤) : Nonempty ((self.functor.obj M).carrier ≃ₗ⁅R,𝔤⁆ TensorProduct R self.V M.carrier)
• block_factoring (Δ : TriangularDecomposition R 𝔤) (theta : ↥Δ.𝔥 →ₗ[R] R) (M : RepGfObj R 𝔤) : ¬HasGenInfChar M theta → ∀ (x : (self.functor.obj M).carrier), x = 0
• is_exact {M₁ M₂ M₃ : RepGfObj R 𝔤} (f : RepGfHom M₁ M₂) (g : RepGfHom M₂ M₃) (_hex : IsExactSequence f g) : IsExactSequence (self.functor.mapHom f) (self.functor.mapHom g)
• sends_projectives_to_projectives (M : RepGfObj R 𝔤) : IsProjectiveModule M → IsProjectiveModule (self.functor.obj M)

structure ProjectiveFunctors.IsProjectiveFunctor {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) : Prop

• exists_tensor_summand : ∃ (FV : TensorFunctorData R 𝔤), IsDirectSummand F FV.functor

theorem ProjectiveFunctors.tensor_functor_is_projective {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (FV : TensorFunctorData R 𝔤) : IsProjectiveFunctor FV.functor

theorem ProjectiveFunctors.IsProjectiveFunctor.is_exact {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {F : EndoFunctorData R 𝔤} (hF : IsProjectiveFunctor F) {M₁ M₂ M₃ : RepGfObj R 𝔤} (f : RepGfHom M₁ M₂) (g : RepGfHom M₂ M₃) (_hex : IsExactSequence f g) : IsExactSequence (F.mapHom f) (F.mapHom g)

theorem ProjectiveFunctors.IsProjectiveFunctor.sends_projectives_to_projectives {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {F : EndoFunctorData R 𝔤} (hF : IsProjectiveFunctor F) (M : RepGfObj R 𝔤) (hM : IsProjectiveModule M) : IsProjectiveModule (F.obj M)

structure ProjectiveFunctors.ThetaFunctorData (R : Type u) [CommRing R] (𝔤 : Type u) [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (theta : ↥Δ.𝔥 →ₗ[R] R) : Type (u + 1)

• baseFunctor : EndoFunctorData R 𝔤
• factors_through_block (M : RepGfObj R 𝔤) : ¬HasGenInfChar M theta → ∀ (x : (self.baseFunctor.obj M).carrier), x = 0

def ProjectiveFunctors.AreNatIsoTheta {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} {theta : ↥Δ.𝔥 →ₗ[R] R} (F G : ThetaFunctorData R 𝔤 Δ wg theta) : Prop

def ProjectiveFunctors.IsDirectSummandTheta {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} {theta : ↥Δ.𝔥 →ₗ[R] R} (F G : ThetaFunctorData R 𝔤 Δ wg theta) : Prop

def ProjectiveFunctors.TensorFunctorData.restrictToTheta {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (FV : TensorFunctorData R 𝔤) (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (theta : ↥Δ.𝔥 →ₗ[R] R) : ThetaFunctorData R 𝔤 Δ wg theta

structure ProjectiveFunctors.IsProjectiveThetaFunctor {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} {theta : ↥Δ.𝔥 →ₗ[R] R} (F : ThetaFunctorData R 𝔤 Δ wg theta) : Prop

• exists_tensor_summand : ∃ (FV : TensorFunctorData R 𝔤), IsDirectSummandTheta F (FV.restrictToTheta Δ wg theta)

def ProjectiveFunctors.NatTransThetaSpace {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : ThetaFunctorData R 𝔤 Δ wg theta) : Type (u + 1)

def ProjectiveFunctors.evalAtVerma {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : ThetaFunctorData R 𝔤 Δ wg theta) (Mverma : RepGfObj R 𝔤) (eta : NatTransThetaSpace F₁ F₂) : RepGfHom (F₁.baseFunctor.obj Mverma) (F₂.baseFunctor.obj Mverma)

theorem ProjectiveFunctors.eilenbergWatts_eval_factorization {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (FV₁ FV₂ : TensorFunctorData R 𝔤) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) : ∃ (X : Type u) (ew : NatTransData FV₁.functor FV₂.functor → X) (dj : X → RepGfHom (FV₁.functor.obj Mverma) (FV₂.functor.obj Mverma)), Function.Bijective ew ∧ Function.Bijective dj ∧ ∀ (η : NatTransData FV₁.functor FV₂.functor), (fun (η : NatTransData FV₁.functor FV₂.functor) => η.app Mverma) η = dj (ew η)

theorem ProjectiveFunctors.dufloJoseph_eval_bijective_at_verma {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (FV₁ FV₂ : TensorFunctorData R 𝔤) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) : Function.Bijective fun (η : NatTransData FV₁.functor FV₂.functor) => η.app Mverma

theorem ProjectiveFunctors.evalAtVerma_bijective_tensor {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (FV₁ FV₂ : TensorFunctorData R 𝔤) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) : Function.Bijective (evalAtVerma (FV₁.restrictToTheta Δ wg lam) (FV₂.restrictToTheta Δ wg lam) Mverma)

theorem ProjectiveFunctors.evalAtVerma_bijective_of_summand {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} {lam : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ G₁ G₂ : ThetaFunctorData R 𝔤 Δ wg lam) (hSum₁ : IsDirectSummandTheta F₁ G₁) (hSum₂ : IsDirectSummandTheta F₂ G₂) (Mverma : RepGfObj R 𝔤) (hBij : Function.Bijective (evalAtVerma G₁ G₂ Mverma)) : Function.Bijective (evalAtVerma F₁ F₂ Mverma)

theorem ProjectiveFunctors.theorem_22_4 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : ThetaFunctorData R 𝔤 Δ wg lam) (_hF₁ : IsProjectiveThetaFunctor F₁) (_hF₂ : IsProjectiveThetaFunctor F₂) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) : Function.Bijective (evalAtVerma F₁ F₂ Mverma)

structure ProjectiveFunctors.NatTransOnInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (theta : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : EndoFunctorData R 𝔤) : Type (u + 1)

• app (M : RepGfObj R 𝔤) : HasInfChar M theta → RepGfHom (F₁.obj M) (F₂.obj M)
• naturality {M₁ M₂ : RepGfObj R 𝔤} (hM₁ : HasInfChar M₁ theta) (hM₂ : HasInfChar M₂ theta) (f : RepGfHom M₁ M₂) : ((self.app M₂ hM₂).comp (F₁.mapHom f)).EqAsMap ((F₂.mapHom f).comp (self.app M₁ hM₁))

structure ProjectiveFunctors.NatTransOnGenInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (theta : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : EndoFunctorData R 𝔤) : Type (u + 1)

• app (M : RepGfObj R 𝔤) : HasGenInfChar M theta → RepGfHom (F₁.obj M) (F₂.obj M)
• naturality {M₁ M₂ : RepGfObj R 𝔤} (hM₁ : HasGenInfChar M₁ theta) (hM₂ : HasGenInfChar M₂ theta) (f : RepGfHom M₁ M₂) : ((self.app M₂ hM₂).comp (F₁.mapHom f)).EqAsMap ((F₂.mapHom f).comp (self.app M₁ hM₁))

def ProjectiveFunctors.NatTransOnGenInfChar.restrictToInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} {F₁ F₂ : EndoFunctorData R 𝔤} (η : NatTransOnGenInfChar theta F₁ F₂) : NatTransOnInfChar theta F₁ F₂

def ProjectiveFunctors.NatTransOnInfChar.EqPointwise {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} {F₁ F₂ : EndoFunctorData R 𝔤} (α β : NatTransOnInfChar theta F₁ F₂) : Prop

def ProjectiveFunctors.NatTransOnInfChar.comp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} {F G H : EndoFunctorData R 𝔤} (β : NatTransOnInfChar theta G H) (α : NatTransOnInfChar theta F G) : NatTransOnInfChar theta F H

def ProjectiveFunctors.NatTransOnInfChar.id {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (theta : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) : NatTransOnInfChar theta F F

def ProjectiveFunctors.AreNatIsoOnInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (theta : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : EndoFunctorData R 𝔤) : Prop

def ProjectiveFunctors.NatTransOnGenInfChar.comp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} {F G H : EndoFunctorData R 𝔤} (β : NatTransOnGenInfChar theta G H) (α : NatTransOnGenInfChar theta F G) : NatTransOnGenInfChar theta F H

def ProjectiveFunctors.NatTransOnGenInfChar.id {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (theta : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) : NatTransOnGenInfChar theta F F

def ProjectiveFunctors.NatTransOnGenInfChar.EqPointwise {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} {F₁ F₂ : EndoFunctorData R 𝔤} (α β : NatTransOnGenInfChar theta F₁ F₂) : Prop

theorem ProjectiveFunctors.genInfChar_admits_infChar_surjection {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (M : RepGfObj R 𝔤) (_hM : HasGenInfChar M theta) : ∃ (N : RepGfObj R 𝔤) (_ : HasInfChar N theta) (f : RepGfHom N M), Function.Surjective ⇑f.toFun

theorem ProjectiveFunctors.exact_functor_preserves_surjection {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) {N M : RepGfObj R 𝔤} (f : RepGfHom N M) (hf : Function.Surjective ⇑f.toFun) : Function.Surjective ⇑(F.mapHom f).toFun

theorem ProjectiveFunctors.genInfChar_generated_by_infChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (M : RepGfObj R 𝔤) (hM : HasGenInfChar M theta) (x : (F.obj M).carrier) : ∃ (N : RepGfObj R 𝔤) (_ : HasInfChar N theta) (f : RepGfHom N M) (y : (F.obj N).carrier), (F.mapHom f).toFun y = x

theorem ProjectiveFunctors.eilenbergWatts_component_lift {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (phi : NatTransOnInfChar theta F₁ F₂) (M : RepGfObj R 𝔤) (hM : HasGenInfChar M theta) : ∃ (phi_hat_M : RepGfHom (F₁.obj M) (F₂.obj M)), ∀ (N : RepGfObj R 𝔤) (hN : HasInfChar N theta) (f : RepGfHom N M) (y : (F₁.obj N).carrier), phi_hat_M.toFun ((F₁.mapHom f).toFun y) = (F₂.mapHom f).toFun ((phi.app N hN).toFun y)

theorem ProjectiveFunctors.eilenbergWatts_homSpace_lift {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (phi : NatTransOnInfChar theta F₁ F₂) : ∃ (phi_hat : NatTransOnGenInfChar theta F₁ F₂), phi_hat.restrictToInfChar.EqPointwise phi

theorem ProjectiveFunctors.homSpace_restriction_surjective {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (phi : NatTransOnInfChar theta F₁ F₂) : ∃ (phi_hat : NatTransOnGenInfChar theta F₁ F₂), ∀ (M : RepGfObj R 𝔤) (hM : HasInfChar M theta) (x : (F₁.obj M).carrier), (phi_hat.app M ⋯).toFun x = (phi.app M hM).toFun x

theorem ProjectiveFunctors.liftInfCharToGenInfChar_exists {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (phi : NatTransOnInfChar theta F₁ F₂) : ∃ (phi_hat : NatTransOnGenInfChar theta F₁ F₂), phi_hat.restrictToInfChar.EqPointwise phi

theorem ProjectiveFunctors.genInfChar_restriction_injective {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (α β : NatTransOnGenInfChar theta F₁ F₂) (hAgree : α.restrictToInfChar.EqPointwise β.restrictToInfChar) : α.EqPointwise β

theorem ProjectiveFunctors.liftInfCharToGenInfChar_idempotent_exists {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (phi : NatTransOnInfChar theta F F) (_hIdem : ∀ (M : RepGfObj R 𝔤) (hM : HasInfChar M theta) (x : (F.obj M).carrier), (phi.app M hM).toFun ((phi.app M hM).toFun x) = (phi.app M hM).toFun x) : ∃ (phi_hat : NatTransOnGenInfChar theta F F), phi_hat.restrictToInfChar.EqPointwise phi ∧ (phi_hat.comp phi_hat).EqPointwise phi_hat

theorem ProjectiveFunctors.proposition_22_5_i {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {_wg : WeylGroupData Δ} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (phi : NatTransOnInfChar theta F₁ F₂) : ∃ (phi_hat : NatTransOnGenInfChar theta F₁ F₂), phi_hat.restrictToInfChar.EqPointwise phi

theorem ProjectiveFunctors.filtration_induction_step {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (η : NatTransOnGenInfChar theta F F) (hRestr : ∀ (N : RepGfObj R 𝔤) (hN : HasInfChar N theta) (y : (F.obj N).carrier), (η.app N ⋯).toFun y = y) (M : RepGfObj R 𝔤) (hM : HasGenInfChar M theta) (x : (F.obj M).carrier) : (η.app M hM).toFun x = x

theorem ProjectiveFunctors.restrictToInfChar_injective {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {theta : ↥Δ.𝔥 →ₗ[R] R} (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (η : NatTransOnGenInfChar theta F F) (hRestr : η.restrictToInfChar.EqPointwise (NatTransOnInfChar.id theta F)) : η.EqPointwise (NatTransOnGenInfChar.id theta F)

theorem ProjectiveFunctors.proposition_22_5_iii {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {_wg : WeylGroupData Δ} {theta : ↥Δ.𝔥 →ₗ[R] R} (F₁ F₂ : EndoFunctorData R 𝔤) (hF₁ : IsProjectiveFunctor F₁) (hF₂ : IsProjectiveFunctor F₂) (phi : NatTransOnInfChar theta F₁ F₂) (psi : NatTransOnInfChar theta F₂ F₁) (hInvL : ∀ (M : RepGfObj R 𝔤) (hM : HasInfChar M theta) (x : (F₁.obj M).carrier), (psi.app M hM).toFun ((phi.app M hM).toFun x) = x) (hInvR : ∀ (M : RepGfObj R 𝔤) (hM : HasInfChar M theta) (x : (F₂.obj M).carrier), (phi.app M hM).toFun ((psi.app M hM).toFun x) = x) : ∃ (phi_hat : NatTransOnGenInfChar theta F₁ F₂) (psi_hat : NatTransOnGenInfChar theta F₂ F₁), phi_hat.restrictToInfChar.EqPointwise phi ∧ psi_hat.restrictToInfChar.EqPointwise psi ∧ (psi_hat.comp phi_hat).EqPointwise (NatTransOnGenInfChar.id theta F₁) ∧ (phi_hat.comp psi_hat).EqPointwise (NatTransOnGenInfChar.id theta F₂)

def ProjectiveFunctors.AreNatIsoOnGenInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (theta : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : EndoFunctorData R 𝔤) : Prop

def ProjectiveFunctors.IsDirectSumDecompObj {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {n : ℕ} (M : RepGfObj R 𝔤) (summands : Fin n → RepGfObj R 𝔤) : Prop

def ProjectiveFunctors.IsIndecomposableObj {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : RepGfObj R 𝔤) : Prop

def ProjectiveFunctors.IsIndecomposable {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) : Prop

def ProjectiveFunctors.IsDirectSumDecomp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) {n : ℕ} (F_i : Fin n → EndoFunctorData R 𝔤) : Prop

def ProjectiveFunctors.IsDirectSumDecompGen {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) {ι : Type u} [Fintype ι] (F_i : ι → EndoFunctorData R 𝔤) : Prop

def ProjectiveFunctors.FactorsThroughBlock {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (F : EndoFunctorData R 𝔤) (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem ProjectiveFunctors.projective_factors_through_block {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) : FactorsThroughBlock Δ F lam

def ProjectiveFunctors.IsProjectiveFunctor.toThetaFunctorData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) (hF : IsProjectiveFunctor F) : ThetaFunctorData R 𝔤 Δ wg lam

theorem ProjectiveFunctors.IsProjectiveFunctor.toIsProjectiveThetaFunctor {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) (hF : IsProjectiveFunctor F) : IsProjectiveThetaFunctor (toThetaFunctorData Δ wg lam F hF)

theorem ProjectiveFunctors.corollary_22_6_i {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) (iso_fwd : RepGfHom (F₁.obj Mverma) (F₂.obj Mverma)) (iso_bwd : RepGfHom (F₂.obj Mverma) (F₁.obj Mverma)) (_hiso₁ : (iso_bwd.comp iso_fwd).EqAsMap (RepGfHom.id (F₁.obj Mverma))) (_hiso₂ : (iso_fwd.comp iso_bwd).EqAsMap (RepGfHom.id (F₂.obj Mverma))) : AreNatIsoOnGenInfChar lam F₁ F₂

theorem ProjectiveFunctors.corollary_22_6_i_areNatIso {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : EndoFunctorData R 𝔤) (_hF₁ : IsProjectiveFunctor F₁) (_hF₂ : IsProjectiveFunctor F₂) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) (iso_fwd : RepGfHom (F₁.obj Mverma) (F₂.obj Mverma)) (iso_bwd : RepGfHom (F₂.obj Mverma) (F₁.obj Mverma)) (_hiso₁ : (iso_bwd.comp iso_fwd).EqAsMap (RepGfHom.id (F₁.obj Mverma))) (_hiso₂ : (iso_fwd.comp iso_bwd).EqAsMap (RepGfHom.id (F₂.obj Mverma))) : AreNatIso F₁ F₂

theorem ProjectiveFunctors.idempotent_lift_gives_functor_decomp (R : Type u) [CommRing R] (𝔤 : Type u) [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) {n : ℕ} (E_i : Fin n → NatTransData F F) (_hIdem : ∀ (i : Fin n), ((E_i i).comp (E_i i)).EqPointwise (E_i i)) (M₀ : RepGfObj R 𝔤) (summands : Fin n → RepGfObj R 𝔤) (_hDecompObj : IsDirectSumDecompObj (F.obj M₀) summands) (_hEvalCompat : ∀ (i : Fin n) (x : (F.obj M₀).carrier), ((E_i i).app M₀).toFun x = (Exists.choose _hDecompObj i).toFun ((⋯.choose i).toFun x)) (_hComplete : ∀ (M : RepGfObj R 𝔤) (x : (F.obj M).carrier), x = ∑ i : Fin n, ((E_i i).app M).toFun x) : ∃ (F_i : Fin n → EndoFunctorData R 𝔤), (∀ (i : Fin n), (F_i i).obj M₀ = summands i) ∧ IsDirectSumDecomp F F_i

theorem ProjectiveFunctors.isDirectSummand_trans {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (A B C : EndoFunctorData R 𝔤) (h1 : IsDirectSummand A B) (h2 : IsDirectSummand B C) : IsDirectSummand A C

theorem ProjectiveFunctors.projective_of_direct_summand (R : Type u) [CommRing R] (𝔤 : Type u) [LieRing 𝔤] [LieAlgebra R 𝔤] (F G : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (_hSummand : IsDirectSummand G F) : IsProjectiveFunctor G

theorem ProjectiveFunctors.isDirectSummand_of_isDirectSumDecomp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) {n : ℕ} (F_i : Fin n → EndoFunctorData R 𝔤) (h : IsDirectSumDecomp F F_i) (i : Fin n) : IsDirectSummand (F_i i) F

theorem ProjectiveFunctors.corollary_22_6_ii {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) (n : ℕ) (summands : Fin n → RepGfObj R 𝔤) (_hDecomp : IsDirectSumDecompObj (F.obj Mverma) summands) : ∃ (F_i : Fin n → EndoFunctorData R 𝔤), (∀ (i : Fin n), IsProjectiveFunctor (F_i i)) ∧ (∀ (i : Fin n), (F_i i).obj Mverma = summands i) ∧ IsDirectSumDecomp F F_i

theorem ProjectiveFunctors.areNatIso_refl {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) : AreNatIso F F

theorem ProjectiveFunctors.corollary_22_6_iii {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (theta : ↥Δ.𝔥 →ₗ[R] R) (H : ThetaFunctorData R 𝔤 Δ wg theta) (_hH : IsProjectiveThetaFunctor H) : ∃ (F : EndoFunctorData R 𝔤) (hF : IsProjectiveFunctor F), AreNatIsoTheta H (IsProjectiveFunctor.toThetaFunctorData Δ wg theta F hF)

theorem ProjectiveFunctors.corollary_22_6 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : (∀ (F₁ F₂ : EndoFunctorData R 𝔤), IsProjectiveFunctor F₁ → IsProjectiveFunctor F₂ → ∀ (Mverma : RepGfObj R 𝔤), Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) → ∀ (iso_fwd : RepGfHom (F₁.obj Mverma) (F₂.obj Mverma)) (iso_bwd : RepGfHom (F₂.obj Mverma) (F₁.obj Mverma)), (iso_bwd.comp iso_fwd).EqAsMap (RepGfHom.id (F₁.obj Mverma)) → (iso_fwd.comp iso_bwd).EqAsMap (RepGfHom.id (F₂.obj Mverma)) → AreNatIsoOnGenInfChar lam F₁ F₂) ∧ (∀ (F : EndoFunctorData R 𝔤), IsProjectiveFunctor F → ∀ (Mverma : RepGfObj R 𝔤), Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) → ∀ (n : ℕ) (summands : Fin n → RepGfObj R 𝔤), IsDirectSumDecompObj (F.obj Mverma) summands → ∃ (F_i : Fin n → EndoFunctorData R 𝔤), (∀ (i : Fin n), IsProjectiveFunctor (F_i i)) ∧ (∀ (i : Fin n), (F_i i).obj Mverma = summands i) ∧ IsDirectSumDecomp F F_i) ∧ ∀ (H : ThetaFunctorData R 𝔤 Δ wg lam), IsProjectiveThetaFunctor H → ∃ (F : EndoFunctorData R 𝔤) (hF : IsProjectiveFunctor F), AreNatIsoTheta H (IsProjectiveFunctor.toThetaFunctorData Δ wg lam F hF)

theorem ProjectiveFunctors.krullSchmidt_repgf {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : RepGfObj R 𝔤) : ∃ (n : ℕ) (summands : Fin n → RepGfObj R 𝔤), IsDirectSumDecompObj M summands ∧ ∀ (i : Fin n), IsIndecomposableObj (summands i)

theorem ProjectiveFunctors.indecomposable_from_corollary {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) (n : ℕ) (summands : Fin n → RepGfObj R 𝔤) (_hDecomp : IsDirectSumDecompObj (F.obj Mverma) summands) (_hSummandsIndecomp : ∀ (i : Fin n), IsIndecomposableObj (summands i)) (F_i : Fin n → EndoFunctorData R 𝔤) (_hFi_proj : ∀ (i : Fin n), IsProjectiveFunctor (F_i i)) (_hFi_eval : ∀ (i : Fin n), (F_i i).obj Mverma = summands i) (_hFi_decomp : IsDirectSumDecomp F F_i) (i : Fin n) : IsIndecomposable (F_i i)

theorem ProjectiveFunctors.isDirectSumDecomp_to_gen {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : EndoFunctorData R 𝔤) {n : ℕ} (F_i : Fin n → EndoFunctorData R 𝔤) (h : IsDirectSumDecomp F F_i) : IsDirectSumDecompGen F fun (j : ULift.{u, 0} (Fin n)) => F_i j.down

theorem ProjectiveFunctors.proposition_22_7_i {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) : ∃ (ι : Type u) (x : Fintype ι) (F_i : ι → EndoFunctorData R 𝔤), (∀ (i : ι), IsProjectiveFunctor (F_i i)) ∧ (∀ (i : ι), IsIndecomposable (F_i i)) ∧ IsDirectSumDecompGen F F_i

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

theorem ProjectiveFunctors.tensor_functor_preserves_categoryO {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (FV : TensorFunctorData R 𝔤) (M : RepGfObj R 𝔤) (hMO : IsCategoryO Δ rd M.carrier) : IsCategoryO Δ rd (FV.functor.obj M).carrier

theorem ProjectiveFunctors.tensor_functor_preserves_projectiveInO {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (FV : TensorFunctorData R 𝔤) (M : RepGfObj R 𝔤) (hMO : IsCategoryO Δ rd M.carrier) (hMproj : IsProjectiveInO rd M.carrier hMO) (hFMO : IsCategoryO Δ rd (FV.functor.obj M).carrier) : IsProjectiveInO rd (FV.functor.obj M).carrier hFMO

theorem ProjectiveFunctors.direct_summand_preserves_categoryO {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (F G : EndoFunctorData R 𝔤) (_hDS : IsDirectSummand F G) (M : RepGfObj R 𝔤) (hGMO : IsCategoryO Δ rd (G.obj M).carrier) : IsCategoryO Δ rd (F.obj M).carrier

theorem ProjectiveFunctors.direct_summand_preserves_projectiveInO {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (F G : EndoFunctorData R 𝔤) (_hDS : IsDirectSummand F G) (M : RepGfObj R 𝔤) (hFMO : IsCategoryO Δ rd (F.obj M).carrier) (hGMO : IsCategoryO Δ rd (G.obj M).carrier) (hGMproj : IsProjectiveInO rd (G.obj M).carrier hGMO) : IsProjectiveInO rd (F.obj M).carrier hFMO

theorem ProjectiveFunctors.projective_functor_preserves_projective_in_O {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hDom : IsDominantWeightLE rd wg lam) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (M : RepGfObj R 𝔤) (_hMO : IsCategoryO Δ rd M.carrier) (_hMproj : IsProjectiveInO rd M.carrier _hMO) : ∃ (hFMO : IsCategoryO Δ rd (F.obj M).carrier), IsProjectiveInO rd (F.obj M).carrier hFMO

theorem ProjectiveFunctors.singular_vector_avoids_radical {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) {P : Type u} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (v : P) (lam : ↥Δ.𝔥 →ₗ[R] R) (hv_ne : v ≠ 0) (hv_weight : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = lam h • v) (hv_killed : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0) (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hPindecomp : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) (J : LieSubmodule R 𝔤 P) (hJ_ne_top : J ≠ ⊤) (hJ_max : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) (hJ_irr : LieModule.IsIrreducible R 𝔤 (P ⧸ J)) : v ∉ J

theorem ProjectiveFunctors.singular_vector_lieSpan_eq_top {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) {P : Type u} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (v : P) (lam : ↥Δ.𝔥 →ₗ[R] R) (hv_ne : v ≠ 0) (hv_weight : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = lam h • v) (hv_killed : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0) (hPO : IsCategoryO Δ rd P) (hPproj : IsProjectiveInO rd P hPO) (hPindecomp : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : LieSubmodule.lieSpan R 𝔤 {v} = ⊤

theorem ProjectiveFunctors.singular_vector_generates_catO {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) {P : Type u} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (v : P) (lam : ↥Δ.𝔥 →ₗ[R] R) (hv_ne : v ≠ 0) (_hv_weight : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = lam h • v) (_hv_killed : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0) (_hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P _hPO) (_hPindecomp : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : LieSubmodule.lieSpan R 𝔤 {v} = ⊤

theorem ProjectiveFunctors.singular_vector_not_in_maximal_submodule {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) {P : Type u} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (v : P) (lam : ↥Δ.𝔥 →ₗ[R] R) (hv_ne : v ≠ 0) (_hv_weight : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = lam h • v) (_hv_killed : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0) (_hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P _hPO) (_hPindecomp : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) (J : LieSubmodule R 𝔤 P) (_hJ_ne_top : J ≠ ⊤) (_hJ_max : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) (_hPJ_irr : LieModule.IsIrreducible R 𝔤 (P ⧸ J)) : v ∉ J

theorem ProjectiveFunctors.singular_vector_generates_indecomp_projective {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) {P : Type u} [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (v : P) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hv_ne : v ≠ 0) (_hv_weight : ∀ (h : ↥Δ.𝔥), ⁅↑h, v⁆ = lam h • v) (_hv_killed : ∀ (e : ↥Δ.𝔫_pos), ⁅↑e, v⁆ = 0) (hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P hPO) (_hPindecomp : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) (J : LieSubmodule R 𝔤 P) (_hJ_ne_top : J ≠ ⊤) (_hJ_max : ∀ (N : LieSubmodule R 𝔤 P), N ≠ ⊤ → N ≤ J) (_hPJ_irr : LieModule.IsIrreducible R 𝔤 (P ⧸ J)) : LieSubmodule.lieSpan R 𝔤 {v} = ⊤

theorem ProjectiveFunctors.indecomposable_projective_in_O_has_highest_weight {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (P : Type u) [AddCommGroup P] [Module R P] [LieRingModule 𝔤 P] [LieModule R 𝔤 P] (hPO : IsCategoryO Δ rd P) (_hPproj : IsProjectiveInO rd P hPO) (_hPindecomp : ∀ (A B : LieSubmodule R 𝔤 P), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) : ∃ (mu : ↥Δ.𝔥 →ₗ[R] R), Nonempty (IsHighestWeightModule Δ P (mu - wg.ρ))

theorem ProjectiveFunctors.lieSubmodule_decomp_gives_idempotent {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (M : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ M.carrier (lam - wg.ρ))) (A B : LieSubmodule R 𝔤 (F.obj M).carrier) (_hInf : A ⊓ B = ⊥) (_hSup : A ⊔ B = ⊤) (hA : A ≠ ⊥) (hB : B ≠ ⊥) : ∃ (e : NatTransData F F), (e.comp e).EqPointwise e ∧ ¬e.EqPointwise (NatTransData.id F) ∧ ¬∀ (N : RepGfObj R 𝔤) (x : (F.obj N).carrier), (e.app N).toFun x = 0

theorem ProjectiveFunctors.functor_indecomp_gives_module_indecomp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hDom : IsDominantWeightLE rd wg lam) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (_hIndecomp : IsIndecomposable F) (_hBlock : FactorsThroughBlock Δ F lam) (M : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ M.carrier (lam - wg.ρ))) (A B : LieSubmodule R 𝔤 (F.obj M).carrier) : A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥

theorem ProjectiveFunctors.verma_isCategoryO {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (M : Type u_1) [AddCommGroup M] [Module R M] [LieRingModule 𝔤 M] [LieModule R 𝔤 M] (wt : ↥Δ.𝔥 →ₗ[R] R) (_hM : IsVermaModule Δ M wt) : IsCategoryO Δ rd M

theorem ProjectiveFunctors.proposition_22_7_ii {R : Type u} [Field R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (rd : PositiveRootData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hDom : IsDominantWeightLE rd wg lam) (F : EndoFunctorData R 𝔤) (_hF : IsProjectiveFunctor F) (_hIndecomp : IsIndecomposable F) (_hBlock : FactorsThroughBlock Δ F lam) (Mverma : RepGfObj R 𝔤) (_hMverma : Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ))) : ∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (hO : IsCategoryO Δ rd (F.obj Mverma).carrier), IsProjectiveInO rd (F.obj Mverma).carrier hO ∧ (∀ (A B : LieSubmodule R 𝔤 (F.obj Mverma).carrier), A ⊓ B = ⊥ → A ⊔ B = ⊤ → A = ⊥ ∨ B = ⊥) ∧ Nonempty (IsHighestWeightModule Δ (F.obj Mverma).carrier (mu - wg.ρ))