structure GrothendieckGroupData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) : Type (u + 1)

• carrier : Type u
• instACG : AddCommGroup self.carrier
• instMod : Module ℤ self.carrier
• delta : (↥Δ.𝔥 →ₗ[R] R) → self.carrier
• pairing : self.carrier → self.carrier → ℤ
• pairing_orthonormal (lam mu : ↥Δ.𝔥 →ₗ[R] R) : self.pairing (self.delta lam) (self.delta mu) = if lam = mu then 1 else 0
• pairing_basis_determines (h₁ h₂ : self.carrier → self.carrier → ℤ) : (∀ (lam mu : ↥Δ.𝔥 →ₗ[R] R), h₁ (self.delta lam) (self.delta mu) = h₂ (self.delta lam) (self.delta mu)) → ∀ (x y : self.carrier), h₁ x y = h₂ x y

structure GrothendieckGroupData.InnerProductData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) : Type u

• pairing : KO.carrier → KO.carrier → ℤ
• orthonormal (lam mu : ↥Δ.𝔥 →ₗ[R] R) : self.pairing (KO.delta lam) (KO.delta mu) = if lam = mu then 1 else 0
• pairing_basis_determines (h₁ h₂ : KO.carrier → KO.carrier → ℤ) : (∀ (lam mu : ↥Δ.𝔥 →ₗ[R] R), h₁ (KO.delta lam) (KO.delta mu) = h₂ (KO.delta lam) (KO.delta mu)) → ∀ (x y : KO.carrier), h₁ x y = h₂ x y

structure InducedMapData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) : Type (u + 1)

• F : ProjectiveFunctors.EndoFunctorData R 𝔤
• hF : ProjectiveFunctors.IsProjectiveFunctor self.F
• mapKO : KO.carrier → KO.carrier
• map_basis_compat (g : KO.carrier → KO.carrier) : (∀ (lam : ↥Δ.𝔥 →ₗ[R] R), g (KO.delta lam) = self.mapKO (KO.delta lam)) → g = self.mapKO

structure WeylActionData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) : Type (max u u_1)

• act : wg.W → KO.carrier → KO.carrier
• act_delta (w : wg.W) (lam : ↥Δ.𝔥 →ₗ[R] R) : self.act w (KO.delta lam) = KO.delta (wg.dualAction w lam)

structure AdjointPairData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] : Type (u + 1)

• F : ProjectiveFunctors.EndoFunctorData R 𝔤
• Fv : ProjectiveFunctors.EndoFunctorData R 𝔤
• hF : ProjectiveFunctors.IsProjectiveFunctor self.F
• hFv : ProjectiveFunctors.IsProjectiveFunctor self.Fv
• adjunction_fwd (M N : ProjectiveFunctors.RepGfObj R 𝔤) : ProjectiveFunctors.RepGfHom (self.F.obj M) N → ProjectiveFunctors.RepGfHom M (self.Fv.obj N)
• adjunction_bwd (M N : ProjectiveFunctors.RepGfObj R 𝔤) : ProjectiveFunctors.RepGfHom M (self.Fv.obj N) → ProjectiveFunctors.RepGfHom (self.F.obj M) N
• adjunction_homDim_pairing {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF fFv : InducedMapData KO) : fF.F = self.F → fFv.F = self.Fv → ∀ (lam mu : ↥Δ.𝔥 →ₗ[R] R), ip.pairing (fF.mapKO (KO.delta lam)) (KO.delta mu) = ip.pairing (fFv.mapKO (KO.delta mu)) (KO.delta lam)

structure AdjointPairDataWeak {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] : Type (u + 1)

• F : ProjectiveFunctors.EndoFunctorData R 𝔤
• Fv : ProjectiveFunctors.EndoFunctorData R 𝔤
• adjunction_fwd (M N : ProjectiveFunctors.RepGfObj R 𝔤) : ProjectiveFunctors.RepGfHom (self.F.obj M) N → ProjectiveFunctors.RepGfHom M (self.Fv.obj N)
• adjunction_bwd (M N : ProjectiveFunctors.RepGfObj R 𝔤) : ProjectiveFunctors.RepGfHom M (self.Fv.obj N) → ProjectiveFunctors.RepGfHom (self.F.obj M) N

def AdjointPairDataWeak.toAdjointPairData {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairDataWeak) (hF : ProjectiveFunctors.IsProjectiveFunctor adj.F) (hFv : ProjectiveFunctors.IsProjectiveFunctor adj.Fv) (hDim : ∀ {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF fFv : InducedMapData KO), fF.F = adj.F → fFv.F = adj.Fv → ∀ (lam mu : ↥Δ.𝔥 →ₗ[R] R), ip.pairing (fF.mapKO (KO.delta lam)) (KO.delta mu) = ip.pairing (fFv.mapKO (KO.delta mu)) (KO.delta lam)) : AdjointPairData

def AdjointPairData.toWeak {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairData) : AdjointPairDataWeak

@[simp]

theorem AdjointPairData.toWeak_F {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairData) : adj.toWeak.F = adj.F

@[simp]

theorem AdjointPairData.toWeak_Fv {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairData) : adj.toWeak.Fv = adj.Fv

def DominatesSet {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) : Prop

structure WeightBilinForm {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) : Type u

• form : (↥Δ.𝔥 →ₗ[R] R) → (↥Δ.𝔥 →ₗ[R] R) → R
• symm (mu nu : ↥Δ.𝔥 →ₗ[R] R) : self.form mu nu = self.form nu mu
• bilin_left (mu₁ mu₂ nu : ↥Δ.𝔥 →ₗ[R] R) : self.form (mu₁ + mu₂) nu = self.form mu₁ nu + self.form mu₂ nu
• weyl_normSq_invariant (w : wg.W) (mu nu : ↥Δ.𝔥 →ₗ[R] R) : self.form (wg.dualAction w mu - wg.dualAction w nu) (wg.dualAction w mu - wg.dualAction w nu) = self.form (mu - nu) (mu - nu)
• pos_semidef [LinearOrder R] [IsStrictOrderedRing R] (mu : ↥Δ.𝔥 →ₗ[R] R) : 0 ≤ self.form mu mu
• form_corootPairing_compat (rd : PositiveRootData Δ) (alpha mu : ↥Δ.𝔥 →ₗ[R] R) : alpha ∈ rd.posRoots → 2 • self.form alpha mu = rd.corootPairing mu alpha * self.form alpha alpha
• dominant_corootPairing_diff_nonneg [LinearOrder R] [IsStrictOrderedRing R] (rd : PositiveRootData Δ) (lam phi alpha : ↥Δ.𝔥 →ₗ[R] R) : IsDominantWeightBruhat rd wg lam → BruhatLE rd phi lam → alpha ∈ rd.posRoots → 0 ≤ rd.corootPairing (lam - phi) alpha
• form_coroot_compat (rd : PositiveRootData Δ) (rs : RootSystemWithReflections rd wg) (alpha mu : ↥Δ.𝔥 →ₗ[R] R) : alpha ∈ rs.allRoots → 2 • self.form alpha mu = mu (rs.coroot alpha) * self.form alpha alpha
• form_posRoot_pos [LinearOrder R] [IsStrictOrderedRing R] (rd : PositiveRootData Δ) (alpha : ↥Δ.𝔥 →ₗ[R] R) : alpha ∈ rd.posRoots → 0 < self.form alpha alpha

theorem WeightBilinForm.form_posRoot_nonneg {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (alpha : ↥Δ.𝔥 →ₗ[R] R) (halpha_pos : alpha ∈ rd.posRoots) : 0 ≤ B.form alpha alpha

theorem WeightBilinForm.form_corootPairing_compat_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (alpha mu : ↥Δ.𝔥 →ₗ[R] R) (halpha : alpha ∈ rd.posRoots) : 2 • B.form alpha mu = rd.corootPairing mu alpha * B.form alpha alpha

theorem dominant_corootPairing_diff_nonneg_ax {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (B : WeightBilinForm wg) (lam phi alpha : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hphi_le : BruhatLE rd phi lam) (halpha_pos : alpha ∈ rd.posRoots) : 0 ≤ rd.corootPairing (lam - phi) alpha

theorem WeightBilinForm.form_posRoot_dominant_diff_nonneg {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (lam phi alpha : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hphi_le : BruhatLE rd phi lam) (halpha_pos : alpha ∈ rd.posRoots) : 0 ≤ B.form alpha (lam - phi)

theorem WeightBilinForm.cross_terms_nonneg {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (lam phi alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hphi_le : BruhatLE rd phi lam) (halpha_pos : alpha ∈ rd.posRoots) (_hn_pos : 0 < n) : 0 ≤ n • B.form alpha (lam - phi) + n • B.form alpha (lam - phi) + n • n • B.form alpha alpha

theorem WeightBilinForm.form_coroot_compat_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (rs : RootSystemWithReflections rd wg) (alpha mu : ↥Δ.𝔥 →ₗ[R] R) (halpha : alpha ∈ rs.allRoots) : 2 • B.form alpha mu = mu (rs.coroot alpha) * B.form alpha alpha

theorem WeightBilinForm.form_posRoot_pos_ax {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (alpha : ↥Δ.𝔥 →ₗ[R] R) (halpha_pos : alpha ∈ rd.posRoots) : 0 < B.form alpha alpha

theorem WeightBilinForm.norm_diff_factor_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (rs : RootSystemWithReflections rd wg) (v alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (halpha : alpha ∈ rs.allRoots) : B.form (v + n • alpha) (v + n • alpha) - B.form v v = ↑n * v (rs.coroot alpha) * B.form alpha alpha + ↑n * ↑n * B.form alpha alpha

theorem WeightBilinForm.norm_eq_coroot_zero {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (rs : RootSystemWithReflections rd wg) (lam b alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (hlam_dom : IsDominantWeightBruhat rd wg lam) (halpha_pos : alpha ∈ rd.posRoots) (hn_pos : 0 < n) (hpair : rd.corootPairing b alpha = ↑n) (h_eq : B.form (lam - b) (lam - b) = B.form (lam - b + n • alpha) (lam - b + n • alpha)) : lam (rs.coroot alpha) = 0

theorem WeightBilinForm.dominant_posRoot_cross_le {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (rd : PositiveRootData Δ) (lam phi alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hphi_le : BruhatLE rd phi lam) (halpha_pos : alpha ∈ rd.posRoots) (hn_pos : 0 < n) : B.form (lam - phi) (lam - phi) ≤ B.form (lam - phi) (lam - phi) + (n • B.form alpha (lam - phi) + n • B.form alpha (lam - phi) + n • n • B.form alpha alpha)

def WeightBilinForm.normSq {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (mu : ↥Δ.𝔥 →ₗ[R] R) : R

structure GrothendieckGroupBlock {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) : Type (max (u + 1) u_1)

• carrier : Type u
• instACG : AddCommGroup self.carrier
• instMod : Module ℤ self.carrier
• delta_w : wg.W → self.carrier
• basis_injective : Function.Injective self.delta_w
• basis_linearIndep (c : wg.W → ℤ) : ∑ w : wg.W, c w • self.delta_w w = 0 → ∀ (w : wg.W), c w = 0

theorem generalized_eigenspace_decomposition_aux {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : ProjectiveFunctors.RepGfObj R 𝔤) : ∃ (lam : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ), ProjectiveFunctors.centerActsNilpotentlyShifted_of_order Δ M lam n

theorem generalized_eigenspace_decomposition {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : ProjectiveFunctors.RepGfObj R 𝔤) : ∃ (lam : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ), ProjectiveFunctors.centerActsNilpotentlyShifted_of_order Δ M lam n

theorem block_decomposition_exists {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (M : ProjectiveFunctors.RepGfObj R 𝔤) : ∃ (lam : ↥Δ.𝔥 →ₗ[R] R), ProjectiveFunctors.HasGenInfChar M lam

theorem projective_same_KO_class_iso {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF₁ : ProjectiveFunctors.IsProjectiveFunctor F₁) (_hF₂ : ProjectiveFunctors.IsProjectiveFunctor F₂) (KO : GrothendieckGroupData Δ) (f₁ f₂ : InducedMapData KO) (_hf₁ : f₁.F = F₁) (_hf₂ : f₂.F = F₂) (h_delta : f₁.mapKO (KO.delta lam) = f₂.mapKO (KO.delta lam)) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (_hVM : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) : ∃ (iso_fwd : ProjectiveFunctors.RepGfHom (F₁.obj Mverma) (F₂.obj Mverma)) (iso_bwd : ProjectiveFunctors.RepGfHom (F₂.obj Mverma) (F₁.obj Mverma)), (iso_bwd.comp iso_fwd).EqAsMap (ProjectiveFunctors.RepGfHom.id (F₁.obj Mverma)) ∧ (iso_fwd.comp iso_bwd).EqAsMap (ProjectiveFunctors.RepGfHom.id (F₂.obj Mverma))

theorem verma_existence_krull_schmidt {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF₁ : ProjectiveFunctors.IsProjectiveFunctor F₁) (_hF₂ : ProjectiveFunctors.IsProjectiveFunctor F₂) (KO : GrothendieckGroupData Δ) (f₁ f₂ : InducedMapData KO) (hf₁ : f₁.F = F₁) (hf₂ : f₂.F = F₂) (h_delta : f₁.mapKO (KO.delta lam) = f₂.mapKO (KO.delta lam)) : ∃ (Mverma : ProjectiveFunctors.RepGfObj R 𝔤), Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) ∧ ∃ (iso_fwd : ProjectiveFunctors.RepGfHom (F₁.obj Mverma) (F₂.obj Mverma)) (iso_bwd : ProjectiveFunctors.RepGfHom (F₂.obj Mverma) (F₁.obj Mverma)), (iso_bwd.comp iso_fwd).EqAsMap (ProjectiveFunctors.RepGfHom.id (F₁.obj Mverma)) ∧ (iso_fwd.comp iso_bwd).EqAsMap (ProjectiveFunctors.RepGfHom.id (F₂.obj Mverma))

theorem block_natiso_of_same_KO_on_delta {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF₁ : ProjectiveFunctors.IsProjectiveFunctor F₁) (_hF₂ : ProjectiveFunctors.IsProjectiveFunctor F₂) (KO : GrothendieckGroupData Δ) (f₁ f₂ : InducedMapData KO) (hf₁ : f₁.F = F₁) (hf₂ : f₂.F = F₂) (h_delta : f₁.mapKO (KO.delta lam) = f₂.mapKO (KO.delta lam)) : ProjectiveFunctors.AreNatIsoOnGenInfChar lam F₁ F₂

theorem block_areNatIso_of_same_KO_on_delta {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF₁ : ProjectiveFunctors.IsProjectiveFunctor F₁) (_hF₂ : ProjectiveFunctors.IsProjectiveFunctor F₂) (KO : GrothendieckGroupData Δ) (f₁ f₂ : InducedMapData KO) (hf₁ : f₁.F = F₁) (hf₂ : f₂.F = F₂) (h_delta : f₁.mapKO (KO.delta lam) = f₂.mapKO (KO.delta lam)) : ProjectiveFunctors.AreNatIso F₁ F₂

theorem hasGenInfChar_of_hom {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M₁ M₂ : ProjectiveFunctors.RepGfObj R 𝔤} (theta : ↥Δ.𝔥 →ₗ[R] R) (_hM₁ : ProjectiveFunctors.HasGenInfChar M₁ theta) (_f : ProjectiveFunctors.RepGfHom M₁ M₂) : ProjectiveFunctors.HasGenInfChar M₂ theta

theorem hasGenInfChar_unique {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {M : ProjectiveFunctors.RepGfObj R 𝔤} {theta₁ theta₂ : ↥Δ.𝔥 →ₗ[R] R} (_h₁ : ProjectiveFunctors.HasGenInfChar M theta₁) (_h₂ : ProjectiveFunctors.HasGenInfChar M theta₂) : theta₁ = theta₂

theorem block_assembly_naturality {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (η_fn : (theta : ↥Δ.𝔥 →ₗ[R] R) → ProjectiveFunctors.NatTransOnGenInfChar theta F₁ F₂) (lam_of : ProjectiveFunctors.RepGfObj R 𝔤 → ↥Δ.𝔥 →ₗ[R] R) (hlam_of : ∀ (M : ProjectiveFunctors.RepGfObj R 𝔤), ProjectiveFunctors.HasGenInfChar M (lam_of M)) {M₁ M₂ : ProjectiveFunctors.RepGfObj R 𝔤} (f : ProjectiveFunctors.RepGfHom M₁ M₂) (x : (F₁.obj M₁).carrier) : ((η_fn (lam_of M₂)).app M₂ ⋯).toFun ((F₁.mapHom f).toFun x) = (F₂.mapHom f).toFun (((η_fn (lam_of M₁)).app M₁ ⋯).toFun x)

theorem areNatIso_of_all_geninfchar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF₁ : ProjectiveFunctors.IsProjectiveFunctor F₁) (_hF₂ : ProjectiveFunctors.IsProjectiveFunctor F₂) (h_blocks : ∀ (lam : ↥Δ.𝔥 →ₗ[R] R), ProjectiveFunctors.AreNatIsoOnGenInfChar lam F₁ F₂) : ProjectiveFunctors.AreNatIso F₁ F₂

theorem theorem_23_1_i {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (f₁ f₂ : InducedMapData KO) (h_eq : f₁.mapKO = f₂.mapKO) : ProjectiveFunctors.AreNatIso f₁.F f₂.F

def homDim {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) : ℤ

theorem hom_multiplicity_eq_pairing {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) : ip.pairing (fF.mapKO (KO.delta lam)) (KO.delta mu) = homDim KO ip fF lam mu

theorem adjunction_preserves_homDim {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (adj : AdjointPairData) (fF fFv : InducedMapData KO) (hfF : fF.F = adj.F) (hfFv : fFv.F = adj.Fv) (lam mu : ↥Δ.𝔥 →ₗ[R] R) : homDim KO ip fF lam mu = homDim KO ip fFv mu lam

theorem adjoint_pair_basis_pairing {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (adj : AdjointPairData) (fF fFv : InducedMapData KO) (hfF : fF.F = adj.F) (hfFv : fFv.F = adj.Fv) (lam mu : ↥Δ.𝔥 →ₗ[R] R) : ip.pairing (fF.mapKO (KO.delta lam)) (KO.delta mu) = ip.pairing (KO.delta lam) (fFv.mapKO (KO.delta mu))

theorem theorem_23_1_ii {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (adj : AdjointPairData) (fF fFv : InducedMapData KO) (hfF : fF.F = adj.F) (hfFv : fFv.F = adj.Fv) (x y : KO.carrier) : ip.pairing (fF.mapKO x) y = ip.pairing x (fFv.mapKO y)

noncomputable def projective_functor_has_induced_map_data {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF : ProjectiveFunctors.IsProjectiveFunctor F) : InducedMapData KO

theorem projective_functor_has_induced_map_data_F {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF : ProjectiveFunctors.IsProjectiveFunctor F) : (projective_functor_has_induced_map_data KO F hF).F = F

theorem projective_functor_has_induced_map_data_unique_on_basis {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF : ProjectiveFunctors.IsProjectiveFunctor F) (d' : InducedMapData KO) (hd' : d'.F = F) (lam : ↥Δ.𝔥 →ₗ[R] R) : d'.mapKO (KO.delta lam) = (projective_functor_has_induced_map_data KO F hF).mapKO (KO.delta lam)

theorem induced_map_delta_determined_by_functor {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (d₁ d₂ : InducedMapData KO) (hF : d₁.F = d₂.F) (lam : ↥Δ.𝔥 →ₗ[R] R) : d₁.mapKO (KO.delta lam) = d₂.mapKO (KO.delta lam)

noncomputable def projective_functor_has_induced_map_data_with_F {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF : ProjectiveFunctors.IsProjectiveFunctor F) : { d : InducedMapData KO // d.F = F ∧ ∀ (d' : InducedMapData KO), d'.F = F → ∀ (lam : ↥Δ.𝔥 →ₗ[R] R), d'.mapKO (KO.delta lam) = d.mapKO (KO.delta lam) }

def grothendieck_group_has_inner_product {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) : KO.InnerProductData

theorem inner_product_nondegen {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (a b : KO.carrier) (h : ∀ (mu : ↥Δ.𝔥 →ₗ[R] R), ip.pairing (KO.delta mu) a = ip.pairing (KO.delta mu) b) : a = b

theorem induced_map_basis_determined_by_functor {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (f₁ f₂ : InducedMapData KO) (h_same_F : f₁.F = f₂.F) (lam : ↥Δ.𝔥 →ₗ[R] R) : f₁.mapKO (KO.delta lam) = f₂.mapKO (KO.delta lam)

theorem induced_map_unique_for_same_functor {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (f₁ f₂ : InducedMapData KO) (h_same_F : f₁.F = f₂.F) : f₁.mapKO = f₂.mapKO

theorem tensor_functor_dual_summand_transfer_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (FV : ProjectiveFunctors.TensorFunctorData R 𝔤) (adj : AdjointPairDataWeak) (h_summand : ProjectiveFunctors.IsDirectSummand adj.F FV.functor) : ∃ (FV_dual : ProjectiveFunctors.TensorFunctorData R 𝔤), ProjectiveFunctors.IsDirectSummand adj.Fv FV_dual.functor

theorem tensor_functor_dual_summand_transfer_rev_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (FV : ProjectiveFunctors.TensorFunctorData R 𝔤) (adj : AdjointPairDataWeak) (h_summand : ProjectiveFunctors.IsDirectSummand adj.Fv FV.functor) : ∃ (FV_dual : ProjectiveFunctors.TensorFunctorData R 𝔤), ProjectiveFunctors.IsDirectSummand adj.F FV_dual.functor

theorem tensor_functor_is_exact_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (FV : ProjectiveFunctors.TensorFunctorData R 𝔤) {M₁ M₂ M₃ : ProjectiveFunctors.RepGfObj R 𝔤} (f : ProjectiveFunctors.RepGfHom M₁ M₂) (g : ProjectiveFunctors.RepGfHom M₂ M₃) (hex : ProjectiveFunctors.IsExactSequence f g) : ProjectiveFunctors.IsExactSequence (FV.functor.mapHom f) (FV.functor.mapHom g)

theorem direct_summand_preserves_exact {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F G : ProjectiveFunctors.EndoFunctorData R 𝔤) (h_summand : ProjectiveFunctors.IsDirectSummand F G) (hG_exact : ∀ {M₁ M₂ M₃ : ProjectiveFunctors.RepGfObj R 𝔤} (f : ProjectiveFunctors.RepGfHom M₁ M₂) (g : ProjectiveFunctors.RepGfHom M₂ M₃), ProjectiveFunctors.IsExactSequence f g → ProjectiveFunctors.IsExactSequence (G.mapHom f) (G.mapHom g)) {M₁ M₂ M₃ : ProjectiveFunctors.RepGfObj R 𝔤} (f : ProjectiveFunctors.RepGfHom M₁ M₂) (g : ProjectiveFunctors.RepGfHom M₂ M₃) (hex : ProjectiveFunctors.IsExactSequence f g) : ProjectiveFunctors.IsExactSequence (F.mapHom f) (F.mapHom g)

theorem directSummand_of_tensor_exact_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (FV : ProjectiveFunctors.TensorFunctorData R 𝔤) (_h : ProjectiveFunctors.IsDirectSummand F FV.functor) {M₁ M₂ M₃ : ProjectiveFunctors.RepGfObj R 𝔤} (f : ProjectiveFunctors.RepGfHom M₁ M₂) (g : ProjectiveFunctors.RepGfHom M₂ M₃) : ProjectiveFunctors.IsExactSequence f g → ProjectiveFunctors.IsExactSequence (F.mapHom f) (F.mapHom g)

theorem directSummand_of_tensor_preserves_proj_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (FV : ProjectiveFunctors.TensorFunctorData R 𝔤) (_h : ProjectiveFunctors.IsDirectSummand F FV.functor) (M : ProjectiveFunctors.RepGfObj R 𝔤) : ProjectiveFunctors.IsProjectiveModule M → ProjectiveFunctors.IsProjectiveModule (F.obj M)

theorem adjoint_projectivity_transfer {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairDataWeak) (hF : ProjectiveFunctors.IsProjectiveFunctor adj.F) : ProjectiveFunctors.IsProjectiveFunctor adj.Fv

theorem adjoint_projectivity_transfer_rev {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairDataWeak) (hFv : ProjectiveFunctors.IsProjectiveFunctor adj.Fv) : ProjectiveFunctors.IsProjectiveFunctor adj.F

theorem adjoint_of_projective_is_projective_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairDataWeak) (G : ProjectiveFunctors.EndoFunctorData R 𝔤) (hG : ProjectiveFunctors.IsProjectiveFunctor G) (hG_eq : G = adj.F ∨ G = adj.Fv) : ProjectiveFunctors.IsProjectiveFunctor adj.F ∧ ProjectiveFunctors.IsProjectiveFunctor adj.Fv

theorem InnerProductData.pairing_symm {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {KO : GrothendieckGroupData Δ} (ip : KO.InnerProductData) (x y : KO.carrier) : ip.pairing x y = ip.pairing y x

theorem mapKO_adjoint_pairing {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairDataWeak) {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF fFv : InducedMapData KO) (hfF : fF.F = adj.F) (hfFv : fFv.F = adj.Fv) (x y : KO.carrier) : ip.pairing (fF.mapKO x) y = ip.pairing x (fFv.mapKO y)

theorem pairing_eq_of_adjunction_weak {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairDataWeak) {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF fFv : InducedMapData KO) (hfF : fF.F = adj.F) (hfFv : fFv.F = adj.Fv) (lam mu : ↥Δ.𝔥 →ₗ[R] R) : homDim KO ip fF lam mu = homDim KO ip fFv mu lam

theorem adjunction_homDim_pairing_of_weak_adj {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (adj : AdjointPairDataWeak) {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF fFv : InducedMapData KO) (hfF : fF.F = adj.F) (hfFv : fFv.F = adj.Fv) (lam mu : ↥Δ.𝔥 →ₗ[R] R) : ip.pairing (fF.mapKO (KO.delta lam)) (KO.delta mu) = ip.pairing (fFv.mapKO (KO.delta mu)) (KO.delta lam)

theorem theorem_23_1_iii {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF : ProjectiveFunctors.IsProjectiveFunctor F) (adjL adjR : AdjointPairDataWeak) (hL : adjL.Fv = F) (hR : adjR.F = F) : ProjectiveFunctors.AreNatIso adjL.F adjR.Fv

theorem theorem_23_1_iii_adjoint_iso {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (KO : GrothendieckGroupData Δ) (F F_L F_R : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF : ProjectiveFunctors.IsProjectiveFunctor F) (adjL adjR : AdjointPairDataWeak) (hL_F : adjL.F = F_L) (hL_Fv : adjL.Fv = F) (hR_F : adjR.F = F) (hR_Fv : adjR.Fv = F_R) : ProjectiveFunctors.AreNatIso F_L F_R

theorem induced_map_commutes_weyl_action {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (wact : WeylActionData wg KO) (fF : InducedMapData KO) (w : wg.W) (x : KO.carrier) : wact.act w (fF.mapKO x) = fF.mapKO (wact.act w x)

theorem lemma_23_3_i {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (wact : WeylActionData wg KO) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (_hdom : DominatesSet rd lam S) (fF : InducedMapData KO) (w : wg.W) (x : KO.carrier) : wact.act w (fF.mapKO x) = fF.mapKO (wact.act w x)

theorem projective_functor_commutes_weyl {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (wact : WeylActionData wg KO) (fF : InducedMapData KO) (w : wg.W) (x : KO.carrier) : wact.act w (fF.mapKO x) = fF.mapKO (wact.act w x)

theorem theorem_23_2 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (wact : WeylActionData wg KO) (fF : InducedMapData KO) (w : wg.W) (x : KO.carrier) : wact.act w (fF.mapKO x) = fF.mapKO (wact.act w x)

theorem finite_dim_module_of_dominant_weight_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (beta : ↥Δ.𝔥 →ₗ[R] R) (hbeta : rd.IsInQPlus beta) : ∃ (FV : ProjectiveFunctors.TensorFunctorData R 𝔤), True

theorem projective_functor_block_component_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF : ProjectiveFunctors.IsProjectiveFunctor F) (lam : ↥Δ.𝔥 →ₗ[R] R) : ∃ (G : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor G ∧ ProjectiveFunctors.FactorsThroughBlock Δ G lam

theorem translation_functor_of_dominant_weight {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (_wg : WeylGroupData Δ) (lam beta : ↥Δ.𝔥 →ₗ[R] R) (hbeta : rd.IsInQPlus beta) : ∃ (G_L : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor G_L ∧ ProjectiveFunctors.FactorsThroughBlock Δ G_L lam

theorem dominatesSet_implies_isDominantWeightLE {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (hdom : DominatesSet rd lam S) (h_orbit : ∀ w ∈ WeylStabilizerModQ rd wg lam, wg.dualAction w lam ∈ S) : IsDominantWeightLE rd wg lam

theorem summand_of_translation_factors_through_block {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (lam : ↥Δ.𝔥 →ₗ[R] R) (G_L : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hG : ProjectiveFunctors.IsProjectiveFunctor G_L) (hG_block : ProjectiveFunctors.FactorsThroughBlock Δ G_L lam) (F_j : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF : ProjectiveFunctors.IsProjectiveFunctor F_j) (_hIndec : ProjectiveFunctors.IsIndecomposable F_j) {ι : Type u} [Fintype ι] (F_i : ι → ProjectiveFunctors.EndoFunctorData R 𝔤) (hDecomp : ProjectiveFunctors.IsDirectSumDecompGen G_L F_i) (j : ι) (hj : F_j = F_i j) : ProjectiveFunctors.FactorsThroughBlock Δ F_j lam

theorem IsInQPlus_antisymm {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (μ : ↥Δ.𝔥 →ₗ[R] R) (hpos : rd.IsInQPlus μ) (hneg : rd.IsInQPlus (-μ)) : μ = 0

theorem theorem_20_13_verma_filtration_coefficients {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (hdom : DominatesSet rd lam S) (mu : ↥Δ.𝔥 →ₗ[R] R) (hmu : mu ∈ S) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (ι : Type u) [Fintype ι] (F_i : ι → ProjectiveFunctors.EndoFunctorData R 𝔤) (hProj : ∀ (i : ι), ProjectiveFunctors.IsProjectiveFunctor (F_i i)) (hIndec : ∀ (i : ι), ProjectiveFunctors.IsIndecomposable (F_i i)) (nu : ι → ↥Δ.𝔥 →ₗ[R] R) (hnu : ∀ (i : ι), Nonempty (IsHighestWeightModule Δ ((F_i i).obj Mverma).carrier (nu i - wg.ρ))) : ∃ (d : ι → (↥Δ.𝔥 →ₗ[R] R) → ℤ), (∀ (j : ι) (γ : ↥Δ.𝔥 →ₗ[R] R), d j γ ≥ 0) ∧ (∀ (j : ι), d j (nu j) = 1) ∧ ∀ (j : ι) (γ : ↥Δ.𝔥 →ₗ[R] R), ¬rd.IsInQPlus (γ - nu j) → d j γ = 0

theorem tensor_product_character_formula_coefficients {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (hdom : DominatesSet rd lam S) (mu : ↥Δ.𝔥 →ₗ[R] R) (hmu : mu ∈ S) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (ι : Type u) [Fintype ι] (F_i : ι → ProjectiveFunctors.EndoFunctorData R 𝔤) (hProj : ∀ (i : ι), ProjectiveFunctors.IsProjectiveFunctor (F_i i)) (hIndec : ∀ (i : ι), ProjectiveFunctors.IsIndecomposable (F_i i)) (nu : ι → ↥Δ.𝔥 →ₗ[R] R) (hnu : ∀ (i : ι), Nonempty (IsHighestWeightModule Δ ((F_i i).obj Mverma).carrier (nu i - wg.ρ))) (d : ι → (↥Δ.𝔥 →ₗ[R] R) → ℤ) (hd_nonneg : ∀ (j : ι) (γ : ↥Δ.𝔥 →ₗ[R] R), d j γ ≥ 0) (hd_diag : ∀ (j : ι), d j (nu j) = 1) (hd_tri : ∀ (j : ι) (γ : ↥Δ.𝔥 →ₗ[R] R), ¬rd.IsInQPlus (γ - nu j) → d j γ = 0) : (∀ (γ : ↥Δ.𝔥 →ₗ[R] R), ¬rd.IsInQPlus (γ - mu) → ∑ j : ι, d j γ = 0) ∧ ∑ j : ι, d j mu ≥ 1

theorem weight_analysis_mu_appears_among_summands {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (hdom : DominatesSet rd lam S) (mu : ↥Δ.𝔥 →ₗ[R] R) (hmu : mu ∈ S) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (ι : Type u) [Fintype ι] (F_i : ι → ProjectiveFunctors.EndoFunctorData R 𝔤) (hProj : ∀ (i : ι), ProjectiveFunctors.IsProjectiveFunctor (F_i i)) (hIndec : ∀ (i : ι), ProjectiveFunctors.IsIndecomposable (F_i i)) (nu : ι → ↥Δ.𝔥 →ₗ[R] R) (hnu : ∀ (i : ι), Nonempty (IsHighestWeightModule Δ ((F_i i).obj Mverma).carrier (nu i - wg.ρ))) : ∃ (j : ι), nu j = mu

theorem weight_analysis_selects_summand {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (hdom : DominatesSet rd lam S) (mu : ↥Δ.𝔥 →ₗ[R] R) (hmu : mu ∈ S) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (ι : Type u) [Fintype ι] (F_i : ι → ProjectiveFunctors.EndoFunctorData R 𝔤) (hProj : ∀ (i : ι), ProjectiveFunctors.IsProjectiveFunctor (F_i i)) (hIndec : ∀ (i : ι), ProjectiveFunctors.IsIndecomposable (F_i i)) (hw_i : ∀ (i : ι), ∃ (hO : IsCategoryO Δ rd ((F_i i).obj Mverma).carrier), IsProjectiveInO rd ((F_i i).obj Mverma).carrier hO ∧ ∃ (nu_i : ↥Δ.𝔥 →ₗ[R] R), Nonempty (IsHighestWeightModule Δ ((F_i i).obj Mverma).carrier (nu_i - wg.ρ))) : ∃ (j : ι) (hO : IsCategoryO Δ rd ((F_i j).obj Mverma).carrier), IsProjectiveInO rd ((F_i j).obj Mverma).carrier hO ∧ Nonempty (IsHighestWeightModule Δ ((F_i j).obj Mverma).carrier (mu - wg.ρ))

theorem weyl_orbit_in_linkage_class {R : Type u} [Field R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (hdom : DominatesSet rd lam S) (w : wg.W) : w ∈ WeylStabilizerModQ rd wg lam → wg.dualAction w lam ∈ S

theorem lemma_23_3_ii {R : Type u} [Field R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (S : Set (↥Δ.𝔥 →ₗ[R] R)) (hdom : DominatesSet rd lam S) (mu : ↥Δ.𝔥 →ₗ[R] R) (hmu : mu ∈ S) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) : ∃ (F_mu : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F_mu ∧ ProjectiveFunctors.IsIndecomposable F_mu ∧ ∃ (hO : IsCategoryO Δ rd (F_mu.obj Mverma).carrier), IsProjectiveInO rd (F_mu.obj Mverma).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (F_mu.obj Mverma).carrier (mu - wg.ρ))

theorem WeightBilinForm.form_zero_left {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (nu : ↥Δ.𝔥 →ₗ[R] R) : B.form 0 nu = 0

theorem WeightBilinForm.form_nsmul_left {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (n : ℕ) (mu nu : ↥Δ.𝔥 →ₗ[R] R) : B.form (n • mu) nu = n • B.form mu nu

theorem WeightBilinForm.form_expand {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (B : WeightBilinForm wg) (v alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) : B.form (v + n • alpha) (v + n • alpha) = B.form v v + (n • B.form alpha v + n • B.form alpha v + n • n • B.form alpha alpha)

theorem norm_sq_dominant_reflection_nonneg_diff {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (B : WeightBilinForm wg) (lam phi alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hphi_le : BruhatLE rd phi lam) (halpha_pos : alpha ∈ rd.posRoots) (hn_pos : 0 < n) : B.normSq (lam - phi) ≤ B.normSq (lam - phi + n • alpha)

theorem norm_sq_single_step_le {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (B : WeightBilinForm wg) (lam a b : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hb_le : BruhatLE rd b lam) (hstep : ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α a b) : B.normSq (lam - b) ≤ B.normSq (lam - a)

theorem corootPairing_eq_coroot_eval_ax {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (μ α : ↥Δ.𝔥 →ₗ[R] R) (hα : α ∈ rs.allRoots) : rd.corootPairing μ α = μ (rs.coroot α)

theorem norm_sq_equality_implies_lam_coroot_zero_ax {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (B : WeightBilinForm wg) (lam b α : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hα_pos : α ∈ rd.posRoots) (hn_pos : 0 < n) (hpair : rd.corootPairing b α = ↑n) (h_eq : B.normSq (lam - b) = B.normSq (lam - b + n • α)) : lam (rs.coroot α) = 0

theorem norm_sq_reflection_equality_weyl_element {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (B : WeightBilinForm wg) (lam b α : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hα_pos : α ∈ rd.posRoots) (hn_pos : 0 < n) (hpair : rd.corootPairing b α = ↑n) (h_eq : B.normSq (lam - b) = B.normSq (lam - b + n • α)) : ∃ w ∈ WeylStabilizer rd wg lam, wg.dualAction w b = b - n • α

theorem norm_sq_single_step_eq {R : Type u} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (B : WeightBilinForm wg) (lam a b : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hstep : ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α a b) (h_eq : B.normSq (lam - b) = B.normSq (lam - a)) : ∃ w ∈ WeylStabilizer rd wg lam, wg.dualAction w b = a

theorem lemma_23_4_i {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (B : WeightBilinForm wg) (lam phi psi : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hBruhat : BruhatLE rd psi phi) (hphi_le_lam : BruhatLE rd phi lam) : B.normSq (lam - phi) ≤ B.normSq (lam - psi)

theorem lemma_23_4_ii {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (rs : RootSystemWithReflections rd wg) (B : WeightBilinForm wg) (lam phi psi : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hBruhat : BruhatLE rd psi phi) (hphi_le_lam : BruhatLE rd phi lam) (h_eq : B.normSq (lam - phi) = B.normSq (lam - psi)) : ∃ w ∈ WeylStabilizer rd wg lam, wg.dualAction w phi = psi

def IsInXi0 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

def IsProperRep {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

def matrixCoeff {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : ℤ

def supportPF {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) : Set ((↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R))

def maximalSupportPF {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wg : WeylGroupData Δ} (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) [LE R] : Set ((↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R))

def WeylOrbitPair {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : Set ((↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R))

theorem matrixCoeff_eq_standardFiltrationMultiplicity {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (_hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (_hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier _hO) (_hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) (phi : ↥Δ.𝔥 →ₗ[R] R) : matrixCoeff KO ip fF phi lam = ↑(standardFiltrationMultiplicity rd wg mu phi)

theorem matrixCoeff_eq_compositionMultiplicity {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (_hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (_hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier _hO) (_hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) (phi : ↥Δ.𝔥 →ₗ[R] R) : matrixCoeff KO ip fF phi lam = ↑(compositionMultiplicity rd wg phi mu)

theorem theorem_20_13_support_bruhat_bound {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) (phi : ↥Δ.𝔥 →ₗ[R] R) (hmem : (phi, lam) ∈ supportPF KO ip fF) : BruhatLE rd mu phi

theorem theorem_20_13_support_bruhat_upper_bound {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (_wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam phi : ↥Δ.𝔥 →ₗ[R] R) (_hmem : (phi, lam) ∈ supportPF KO ip fF) : BruhatLE rd phi lam

theorem lemma_23_7_bruhat_bound {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (_B : WeightBilinForm wg) (_hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (_hlam_dom : IsDominantWeightBruhat rd wg lam) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) (phi : ↥Δ.𝔥 →ₗ[R] R) (hmem : (phi, lam) ∈ supportPF KO ip fF) : BruhatLE rd mu phi

theorem theorem_20_13_self_multiplicity_pos {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (_wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma : IsVermaModule Δ Mverma.carrier (lam - _wg.ρ)) (_hO : IsCategoryO Δ _rd (fF.F.obj Mverma).carrier) (_hProj : IsProjectiveInO _rd (fF.F.obj Mverma).carrier _hO) (_hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - _wg.ρ))) : matrixCoeff KO ip fF mu lam > 0

theorem mu_lam_positive_matrixCoeff {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) : (mu, lam) ∈ supportPF KO ip fF

theorem block_support_invariant_agree {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (_hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (q : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) (_hq : q ∈ supportPF KO ip fF) (p : ↥wg.invariantSubalgebra) : (evalWeight Δ lam) ↑p = (evalWeight Δ q.2) ↑p

theorem support_second_component_weyl_orbit {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (_hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (q : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) (_hq : q ∈ supportPF KO ip fF) : ∃ (w : wg.W), q.2 = wg.dualAction w lam

theorem matrixCoeff_dualAction_invariant {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (w : wg.W) (mu lam : ↥Δ.𝔥 →ₗ[R] R) : matrixCoeff KO ip fF (wg.dualAction w mu) (wg.dualAction w lam) = matrixCoeff KO ip fF mu lam

theorem support_weyl_equivariant_inv {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (w : wg.W) (a b : ↥Δ.𝔥 →ₗ[R] R) (_hab : (a, b) ∈ supportPF KO ip fF) : (wg.dualAction w⁻¹ a, wg.dualAction w⁻¹ b) ∈ supportPF KO ip fF

theorem bilinForm_weyl_normSq_invariant {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (B : WeightBilinForm wg) (w : wg.W) (mu nu : ↥Δ.𝔥 →ₗ[R] R) : B.normSq (wg.dualAction w mu - wg.dualAction w nu) = B.normSq (mu - nu)

theorem support_reduce_to_lam_fiber {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (_hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (q : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) (hq : q ∈ supportPF KO ip fF) : ∃ (phi : ↥Δ.𝔥 →ₗ[R] R), (phi, lam) ∈ supportPF KO ip fF ∧ B.normSq (q.2 - q.1) = B.normSq (lam - phi)

theorem support_norm_bounded_by_mu_lam {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) (q : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) (hq : q ∈ supportPF KO ip fF) : B.normSq (q.2 - q.1) ≤ B.normSq (lam - mu)

theorem lemma_23_7_mu_lam_in_maxsupp {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) : (mu, lam) ∈ maximalSupportPF KO ip fF B

theorem lemma_23_7_weyl_equivariant {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (rd : PositiveRootData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hmem : (mu, lam) ∈ maximalSupportPF KO ip fF B) (w : wg.W) : (wg.dualAction w mu, wg.dualAction w lam) ∈ maximalSupportPF KO ip fF B

theorem hw_module_implies_linked {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (_KO : GrothendieckGroupData Δ) (fF : InducedMapData _KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (_hO : IsCategoryO Δ _rd (fF.F.obj Mverma).carrier) (_hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) : ∃ (w : wg.W), mu = wg.dualAction w lam

theorem weyl_orbit_implies_isInXi0 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (_hlinked : ∃ (w : wg.W), mu = wg.dualAction w lam) : IsInXi0 rd mu lam

theorem projective_functor_support_in_xi0 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (_wg : WeylGroupData Δ) (_KO : GrothendieckGroupData Δ) (fF : InducedMapData _KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma : IsVermaModule Δ Mverma.carrier (lam - _wg.ρ)) (_hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (_hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - _wg.ρ))) : IsInXi0 rd mu lam

theorem lemma_23_7_in_xi0 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (KO : GrothendieckGroupData Δ) (_ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) : IsInXi0 rd mu lam

theorem support_pair_weyl_decompose {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (_rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (_hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (p : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) (hp : p ∈ supportPF KO ip fF) : ∃ (w : wg.W) (phi : ↥Δ.𝔥 →ₗ[R] R), (phi, lam) ∈ supportPF KO ip fF ∧ p = (wg.dualAction w phi, wg.dualAction w lam)

theorem normSq_weyl_invariant {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (B : WeightBilinForm wg) (a b : ↥Δ.𝔥 →ₗ[R] R) (w : wg.W) : B.normSq (wg.dualAction w a - wg.dualAction w b) = B.normSq (a - b)

theorem support_stabilizer_in_lam_fiber {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (_hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (hmu_supp : (mu, lam) ∈ supportPF KO ip fF) (w : wg.W) (hw_stab : w ∈ WeylStabilizer rd wg lam) : (wg.dualAction w mu, lam) ∈ supportPF KO ip fF

theorem weylStabilizer_fixes_dominant_lam {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] [LinearOrder R] [IsStrictOrderedRing R] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hlam_dom : IsDominantWeightBruhat rd wg lam) (w : wg.W) (hw_stab : w ∈ WeylStabilizer rd wg lam) : wg.dualAction w lam = lam

theorem lemma_23_7_maxsupp_subset_orbit {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) (hmu_in_max : (mu, lam) ∈ maximalSupportPF KO ip fF B) (p : (↥Δ.𝔥 →ₗ[R] R) × (↥Δ.𝔥 →ₗ[R] R)) (hp : p ∈ maximalSupportPF KO ip fF B) : p ∈ WeylOrbitPair wg mu lam

theorem lemma_23_7_mu_minimal {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (_hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (_hlam_dom : IsDominantWeightBruhat rd wg lam) (hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) (hmu_in_max : (mu, lam) ∈ maximalSupportPF KO ip fF B) (w : wg.W) (hw_stab : w ∈ WeylStabilizer rd wg lam) : BruhatLE rd mu (wg.dualAction w mu)

theorem lemma_23_7 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) : maximalSupportPF KO ip fF B = WeylOrbitPair wg mu lam ∧ IsProperRep rd wg mu lam

def SameInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (nu lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

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

theorem proper_rep_implies_bruhatLE {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hproper : IsProperRep rd wg mu lam) : BruhatLE rd mu lam

theorem proper_rep_linkage_class_exists {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hproper : IsProperRep rd wg mu lam) : ∃ (S : Set (↥Δ.𝔥 →ₗ[R] R)), DominatesSet rd lam S ∧ mu ∈ S

theorem block_projection_idempotent_exists {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF : ProjectiveFunctors.IsProjectiveFunctor F) (theta : ↥Δ.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightBruhat rd wg theta) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma : IsVermaModule Δ Mverma.carrier (theta - wg.ρ)) (_hO : IsCategoryO Δ rd (F.obj Mverma).carrier) : ∃ (e_theta : ProjectiveFunctors.NatTransData F F), (e_theta.comp e_theta).EqPointwise e_theta ∧ (∀ (M : ProjectiveFunctors.RepGfObj R 𝔤), ¬ProjectiveFunctors.HasGenInfChar M theta → ∀ (x : (F.obj M).carrier), (e_theta.app M).toFun x = 0) ∧ ∃ (y : (F.obj Mverma).carrier), (e_theta.app Mverma).toFun y ≠ 0

theorem indec_proj_factors_through_block {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (F_xi : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF : ProjectiveFunctors.IsProjectiveFunctor F_xi) (_hI : ProjectiveFunctors.IsIndecomposable F_xi) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightBruhat rd wg lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) (_hO : IsCategoryO Δ rd (F_xi.obj Mverma_lam).carrier) : ProjectiveFunctors.FactorsThroughBlock Δ F_xi lam

theorem verma_hasGenInfChar_of_weight {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma_nu : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)) : ProjectiveFunctors.HasGenInfChar Mverma_nu nu

theorem genInfChar_determines_orbit {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (theta1 theta2 : ↥Δ.𝔥 →ₗ[R] R) (M : ProjectiveFunctors.RepGfObj R 𝔤) (_h1 : ProjectiveFunctors.HasGenInfChar M theta1) (_h2 : ProjectiveFunctors.HasGenInfChar M theta2) : SameInfChar wg theta1 theta2

theorem verma_wrong_infchar_not_hasGenInfChar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (wg : WeylGroupData Δ) (lam nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma_nu : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)) (hne : ¬SameInfChar wg nu lam) : ¬ProjectiveFunctors.HasGenInfChar Mverma_nu lam

theorem indec_proj_annihilates_wrong_infchar {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (F_xi : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF : ProjectiveFunctors.IsProjectiveFunctor F_xi) (_hI : ProjectiveFunctors.IsIndecomposable F_xi) (lam : ↥Δ.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightBruhat rd wg lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (_hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) (_hO : IsCategoryO Δ rd (F_xi.obj Mverma_lam).carrier) (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) : ∀ (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F_xi.obj Mverma_nu)

theorem exists_indec_projFunctor_of_properRep {R : Type u} [Field R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hproper : IsProperRep rd wg mu lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) : ∃ (F_xi : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F_xi ∧ ProjectiveFunctors.IsIndecomposable F_xi ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F_xi.obj Mverma_nu)) ∧ ∃ (hO : IsCategoryO Δ rd (F_xi.obj Mverma_lam).carrier), IsProjectiveInO rd (F_xi.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (F_xi.obj Mverma_lam).carrier (mu - wg.ρ))

theorem projective_cover_unique {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (P₁ P₂ : ProjectiveFunctors.RepGfObj R 𝔤) (_mu : ↥Δ.𝔥 →ₗ[R] R) (hO₁ : IsCategoryO Δ rd P₁.carrier) (_hProj₁ : IsProjectiveInO rd P₁.carrier hO₁) (_hHW₁ : Nonempty (IsHighestWeightModule Δ P₁.carrier (_mu - wg.ρ))) (hO₂ : IsCategoryO Δ rd P₂.carrier) (_hProj₂ : IsProjectiveInO rd P₂.carrier hO₂) (_hHW₂ : Nonempty (IsHighestWeightModule Δ P₂.carrier (_mu - wg.ρ))) : ∃ (iso_fwd : ProjectiveFunctors.RepGfHom P₁ P₂) (iso_bwd : ProjectiveFunctors.RepGfHom P₂ P₁), (iso_bwd.comp iso_fwd).EqAsMap (ProjectiveFunctors.RepGfHom.id P₁) ∧ (iso_fwd.comp iso_bwd).EqAsMap (ProjectiveFunctors.RepGfHom.id P₂)

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

theorem indec_projFunctor_natIso_of_same_properRep {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF₁ : ProjectiveFunctors.IsProjectiveFunctor F₁) (hF₂ : ProjectiveFunctors.IsProjectiveFunctor F₂) (hI₁ : ProjectiveFunctors.IsIndecomposable F₁) (hI₂ : ProjectiveFunctors.IsIndecomposable F₂) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (_hproper : IsProperRep rd wg mu lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) (_hAnnihil₁ : ∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₁.obj Mverma_nu)) (_hAnnihil₂ : ∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₂.obj Mverma_nu)) (hO₁ : IsCategoryO Δ rd (F₁.obj Mverma_lam).carrier) (hProj₁ : IsProjectiveInO rd (F₁.obj Mverma_lam).carrier hO₁) (hHW₁ : Nonempty (IsHighestWeightModule Δ (F₁.obj Mverma_lam).carrier (mu - wg.ρ))) (hO₂ : IsCategoryO Δ rd (F₂.obj Mverma_lam).carrier) (hProj₂ : IsProjectiveInO rd (F₂.obj Mverma_lam).carrier hO₂) (hHW₂ : Nonempty (IsHighestWeightModule Δ (F₂.obj Mverma_lam).carrier (mu - wg.ρ))) : ProjectiveFunctors.AreNatIso F₁ F₂

theorem projective_functor_same_hw_for_same_weight_verma {R : Type u} [Field R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (_hF : ProjectiveFunctors.IsProjectiveFunctor F) (_hI : ProjectiveFunctors.IsIndecomposable F) (lam : ↥Δ.𝔥 →ₗ[R] R) (M₁ M₂ : ProjectiveFunctors.RepGfObj R 𝔤) (_hV₁ : IsVermaModule Δ M₁.carrier (lam - wg.ρ)) (_hV₂ : IsVermaModule Δ M₂.carrier (lam - wg.ρ)) (mu₁ mu₂ : ↥Δ.𝔥 →ₗ[R] R) (_hO₁ : IsCategoryO Δ rd (F.obj M₁).carrier) (_hHW₁ : Nonempty (IsHighestWeightModule Δ (F.obj M₁).carrier (mu₁ - wg.ρ))) (_hO₂ : IsCategoryO Δ rd (F.obj M₂).carrier) (_hHW₂ : Nonempty (IsHighestWeightModule Δ (F.obj M₂).carrier (mu₂ - wg.ρ))) : mu₁ = mu₂

theorem indecomp_proj_functor_gives_proper_pair {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (B : WeightBilinForm wg) (fF : InducedMapData KO) (_hI : ProjectiveFunctors.IsIndecomposable fF.F) (lam0 : ↥Δ.𝔥 →ₗ[R] R) (hlam0_dom : IsDominantWeightBruhat rd wg lam0) (Mverma0 : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma0 : IsVermaModule Δ Mverma0.carrier (lam0 - wg.ρ)) (hO0 : IsCategoryO Δ rd (fF.F.obj Mverma0).carrier) : ∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (lam : ↥Δ.𝔥 →ₗ[R] R), IsProperRep rd wg mu lam ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (fF.F.obj Mverma_nu)) ∧ ∀ (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)), ∃ (hO : IsCategoryO Δ rd (fF.F.obj Mverma_lam).carrier), IsProjectiveInO rd (fF.F.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma_lam).carrier (mu - wg.ρ))

theorem indec_proj_functor_exists_dominant_image {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (B : WeightBilinForm wg) (fF : InducedMapData KO) (_hI : ProjectiveFunctors.IsIndecomposable fF.F) (lam0 : ↥Δ.𝔥 →ₗ[R] R) (hlam0_dom : IsDominantWeightBruhat rd wg lam0) (Mverma0 : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma0 : IsVermaModule Δ Mverma0.carrier (lam0 - wg.ρ)) (hO0 : IsCategoryO Δ rd (fF.F.obj Mverma0).carrier) : ∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (lam : ↥Δ.𝔥 →ₗ[R] R) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤), IsDominantWeightBruhat rd wg lam ∧ Nonempty (IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) ∧ ∃ (hO : IsCategoryO Δ rd (fF.F.obj Mverma_lam).carrier), IsProjectiveInO rd (fF.F.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma_lam).carrier (mu - wg.ρ))

theorem indec_projFunctor_has_properRep {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (B : WeightBilinForm wg) (fF : InducedMapData KO) (hI : ProjectiveFunctors.IsIndecomposable fF.F) (lam0 : ↥Δ.𝔥 →ₗ[R] R) (hlam0_dom : IsDominantWeightBruhat rd wg lam0) (Mverma0 : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma0 : IsVermaModule Δ Mverma0.carrier (lam0 - wg.ρ)) (hO0 : IsCategoryO Δ rd (fF.F.obj Mverma0).carrier) : ∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (lam : ↥Δ.𝔥 →ₗ[R] R), IsProperRep rd wg mu lam ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (fF.F.obj Mverma_nu)) ∧ ∀ (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)), ∃ (hO : IsCategoryO Δ rd (fF.F.obj Mverma_lam).carrier), IsProjectiveInO rd (fF.F.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma_lam).carrier (mu - wg.ρ))

@[reducible, inline]

abbrev theorem_23_6_existence {R : Type u_1} [Field R] {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hproper : IsProperRep rd wg mu lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) : ∃ (F_xi : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F_xi ∧ ProjectiveFunctors.IsIndecomposable F_xi ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F_xi.obj Mverma_nu)) ∧ ∃ (hO : IsCategoryO Δ rd (F_xi.obj Mverma_lam).carrier), IsProjectiveInO rd (F_xi.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (F_xi.obj Mverma_lam).carrier (mu - wg.ρ))

@[reducible, inline]

abbrev theorem_23_6_uniqueness {R : Type u_1} [CommRing R] {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤) (hF₁ : ProjectiveFunctors.IsProjectiveFunctor F₁) (hF₂ : ProjectiveFunctors.IsProjectiveFunctor F₂) (hI₁ : ProjectiveFunctors.IsIndecomposable F₁) (hI₂ : ProjectiveFunctors.IsIndecomposable F₂) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (_hproper : IsProperRep rd wg mu lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) (_hAnnihil₁ : ∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₁.obj Mverma_nu)) (_hAnnihil₂ : ∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₂.obj Mverma_nu)) (hO₁ : IsCategoryO Δ rd (F₁.obj Mverma_lam).carrier) (hProj₁ : IsProjectiveInO rd (F₁.obj Mverma_lam).carrier hO₁) (hHW₁ : Nonempty (IsHighestWeightModule Δ (F₁.obj Mverma_lam).carrier (mu - wg.ρ))) (hO₂ : IsCategoryO Δ rd (F₂.obj Mverma_lam).carrier) (hProj₂ : IsProjectiveInO rd (F₂.obj Mverma_lam).carrier hO₂) (hHW₂ : Nonempty (IsHighestWeightModule Δ (F₂.obj Mverma_lam).carrier (mu - wg.ρ))) : ProjectiveFunctors.AreNatIso F₁ F₂

@[reducible, inline]

abbrev theorem_23_6_surjectivity {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (B : WeightBilinForm wg) (fF : InducedMapData KO) (hI : ProjectiveFunctors.IsIndecomposable fF.F) (lam0 : ↥Δ.𝔥 →ₗ[R] R) (hlam0_dom : IsDominantWeightBruhat rd wg lam0) (Mverma0 : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma0 : IsVermaModule Δ Mverma0.carrier (lam0 - wg.ρ)) (hO0 : IsCategoryO Δ rd (fF.F.obj Mverma0).carrier) : ∃ (mu : ↥Δ.𝔥 →ₗ[R] R) (lam : ↥Δ.𝔥 →ₗ[R] R), IsProperRep rd wg mu lam ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (fF.F.obj Mverma_nu)) ∧ ∀ (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)), ∃ (hO : IsCategoryO Δ rd (fF.F.obj Mverma_lam).carrier), IsProjectiveInO rd (fF.F.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma_lam).carrier (mu - wg.ρ))

theorem indec_projFunctor_classification {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (B : WeightBilinForm wg) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hproper : IsProperRep rd wg mu lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) : (∃ (F_xi : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F_xi ∧ ProjectiveFunctors.IsIndecomposable F_xi ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F_xi.obj Mverma_nu)) ∧ ∃ (hO : IsCategoryO Δ rd (F_xi.obj Mverma_lam).carrier), IsProjectiveInO rd (F_xi.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (F_xi.obj Mverma_lam).carrier (mu - wg.ρ))) ∧ (∀ (fF : InducedMapData KO), ProjectiveFunctors.IsIndecomposable fF.F → ∀ (lam0 : ↥Δ.𝔥 →ₗ[R] R), IsDominantWeightBruhat rd wg lam0 → ∀ (Mverma0 : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma0.carrier (lam0 - wg.ρ)), IsCategoryO Δ rd (fF.F.obj Mverma0).carrier → ∃ (mu' : ↥Δ.𝔥 →ₗ[R] R) (lam' : ↥Δ.𝔥 →ₗ[R] R), IsProperRep rd wg mu' lam' ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam' → IsZeroRepGfObj (fF.F.obj Mverma_nu)) ∧ ∀ (Mverma_lam' : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_lam'.carrier (lam' - wg.ρ)), ∃ (hO : IsCategoryO Δ rd (fF.F.obj Mverma_lam').carrier), IsProjectiveInO rd (fF.F.obj Mverma_lam').carrier hO ∧ Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma_lam').carrier (mu' - wg.ρ))) ∧ ∀ (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F₁ → ProjectiveFunctors.IsProjectiveFunctor F₂ → ProjectiveFunctors.IsIndecomposable F₁ → ProjectiveFunctors.IsIndecomposable F₂ → (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₁.obj Mverma_nu)) → (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₂.obj Mverma_nu)) → (∃ (hO₁ : IsCategoryO Δ rd (F₁.obj Mverma_lam).carrier), IsProjectiveInO rd (F₁.obj Mverma_lam).carrier hO₁ ∧ Nonempty (IsHighestWeightModule Δ (F₁.obj Mverma_lam).carrier (mu - wg.ρ))) → (∃ (hO₂ : IsCategoryO Δ rd (F₂.obj Mverma_lam).carrier), IsProjectiveInO rd (F₂.obj Mverma_lam).carrier hO₂ ∧ Nonempty (IsHighestWeightModule Δ (F₂.obj Mverma_lam).carrier (mu - wg.ρ))) → ProjectiveFunctors.AreNatIso F₁ F₂

@[reducible, inline]

abbrev theorem_23_6_combined {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u_1} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (B : WeightBilinForm wg) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hproper : IsProperRep rd wg mu lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) : (∃ (F_xi : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F_xi ∧ ProjectiveFunctors.IsIndecomposable F_xi ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F_xi.obj Mverma_nu)) ∧ ∃ (hO : IsCategoryO Δ rd (F_xi.obj Mverma_lam).carrier), IsProjectiveInO rd (F_xi.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (F_xi.obj Mverma_lam).carrier (mu - wg.ρ))) ∧ (∀ (fF : InducedMapData KO), ProjectiveFunctors.IsIndecomposable fF.F → ∀ (lam0 : ↥Δ.𝔥 →ₗ[R] R), IsDominantWeightBruhat rd wg lam0 → ∀ (Mverma0 : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma0.carrier (lam0 - wg.ρ)), IsCategoryO Δ rd (fF.F.obj Mverma0).carrier → ∃ (mu' : ↥Δ.𝔥 →ₗ[R] R) (lam' : ↥Δ.𝔥 →ₗ[R] R), IsProperRep rd wg mu' lam' ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam' → IsZeroRepGfObj (fF.F.obj Mverma_nu)) ∧ ∀ (Mverma_lam' : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_lam'.carrier (lam' - wg.ρ)), ∃ (hO : IsCategoryO Δ rd (fF.F.obj Mverma_lam').carrier), IsProjectiveInO rd (fF.F.obj Mverma_lam').carrier hO ∧ Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma_lam').carrier (mu' - wg.ρ))) ∧ ∀ (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F₁ → ProjectiveFunctors.IsProjectiveFunctor F₂ → ProjectiveFunctors.IsIndecomposable F₁ → ProjectiveFunctors.IsIndecomposable F₂ → (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₁.obj Mverma_nu)) → (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F₂.obj Mverma_nu)) → (∃ (hO₁ : IsCategoryO Δ rd (F₁.obj Mverma_lam).carrier), IsProjectiveInO rd (F₁.obj Mverma_lam).carrier hO₁ ∧ Nonempty (IsHighestWeightModule Δ (F₁.obj Mverma_lam).carrier (mu - wg.ρ))) → (∃ (hO₂ : IsCategoryO Δ rd (F₂.obj Mverma_lam).carrier), IsProjectiveInO rd (F₂.obj Mverma_lam).carrier hO₂ ∧ Nonempty (IsHighestWeightModule Δ (F₂.obj Mverma_lam).carrier (mu - wg.ρ))) → ProjectiveFunctors.AreNatIso F₁ F₂

theorem indec_projFunctor_maxSupp_eq_weylOrbit {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (fF : InducedMapData KO) (B : WeightBilinForm wg) (rs : RootSystemWithReflections rd wg) (hFI : ProjectiveFunctors.IsIndecomposable fF.F) (lam mu : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantWeightBruhat rd wg lam) (hFblock : ProjectiveFunctors.FactorsThroughBlock Δ fF.F lam) (Mverma : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma : IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) (hO : IsCategoryO Δ rd (fF.F.obj Mverma).carrier) (hProj : IsProjectiveInO rd (fF.F.obj Mverma).carrier hO) (hHW : Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma).carrier (mu - wg.ρ))) : maximalSupportPF KO ip fF B ⊆ WeylOrbitPair wg mu lam ∧ IsProperRep rd wg mu lam

theorem indec_projFunctor_bijection_xi {R : Type u} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (rs : RootSystemWithReflections rd wg) (KO : GrothendieckGroupData Δ) (ip : KO.InnerProductData) (B : WeightBilinForm wg) (mu lam : ↥Δ.𝔥 →ₗ[R] R) (hproper : IsProperRep rd wg mu lam) (Mverma_lam : ProjectiveFunctors.RepGfObj R 𝔤) (hVerma_lam : IsVermaModule Δ Mverma_lam.carrier (lam - wg.ρ)) : (∃ (F_xi : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F_xi ∧ ProjectiveFunctors.IsIndecomposable F_xi ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (F_xi.obj Mverma_nu)) ∧ (∃ (hO : IsCategoryO Δ rd (F_xi.obj Mverma_lam).carrier), IsProjectiveInO rd (F_xi.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (F_xi.obj Mverma_lam).carrier (mu - wg.ρ))) ∧ ∀ (G : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor G → ProjectiveFunctors.IsIndecomposable G → (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam → IsZeroRepGfObj (G.obj Mverma_nu)) → (∃ (hO : IsCategoryO Δ rd (G.obj Mverma_lam).carrier), IsProjectiveInO rd (G.obj Mverma_lam).carrier hO ∧ Nonempty (IsHighestWeightModule Δ (G.obj Mverma_lam).carrier (mu - wg.ρ))) → ProjectiveFunctors.AreNatIso F_xi G) ∧ ∀ (fF : InducedMapData KO), ProjectiveFunctors.IsIndecomposable fF.F → ∀ (lam0 : ↥Δ.𝔥 →ₗ[R] R), IsDominantWeightBruhat rd wg lam0 → ∀ (Mverma0 : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma0.carrier (lam0 - wg.ρ)), IsCategoryO Δ rd (fF.F.obj Mverma0).carrier → ∃ (mu' : ↥Δ.𝔥 →ₗ[R] R) (lam' : ↥Δ.𝔥 →ₗ[R] R), IsProperRep rd wg mu' lam' ∧ (∀ (nu : ↥Δ.𝔥 →ₗ[R] R) (Mverma_nu : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_nu.carrier (nu - wg.ρ)), ¬SameInfChar wg nu lam' → IsZeroRepGfObj (fF.F.obj Mverma_nu)) ∧ ∀ (Mverma_lam' : ProjectiveFunctors.RepGfObj R 𝔤) (a : IsVermaModule Δ Mverma_lam'.carrier (lam' - wg.ρ)), ∃ (hO : IsCategoryO Δ rd (fF.F.obj Mverma_lam').carrier), IsProjectiveInO rd (fF.F.obj Mverma_lam').carrier hO ∧ Nonempty (IsHighestWeightModule Δ (fF.F.obj Mverma_lam').carrier (mu' - wg.ρ))

theorem multiplicity_free_wall_crossing {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (C : CoxeterGroupData) (KOB : GrothendieckGroupBlock Δ wg) (s : C.W) (_hs : s ∈ C.simpleReflections) (fF_mapKO : KOB.carrier → KOB.carrier) (compat : CoxeterWeylCompatibility C rd wg) (wact : wg.W → KOB.carrier → KOB.carrier) (fF_equivariant : ∀ (w_act : wg.W) (x : KOB.carrier), wact w_act (fF_mapKO x) = fF_mapKO (wact w_act x)) (wact_basis : ∀ (w_act v : wg.W), wact w_act (KOB.delta_w v) = KOB.delta_w (w_act * v)) (wact_add : ∀ (w_act : wg.W) (x y : KOB.carrier), wact w_act (x + y) = wact w_act x + wact w_act y) (fF_base : fF_mapKO (KOB.delta_w 1) = KOB.delta_w 1 + KOB.delta_w (compat.ι s)) (w : C.W) : fF_mapKO (KOB.delta_w (compat.ι w)) = KOB.delta_w (compat.ι w) + KOB.delta_w (compat.ι w * compat.ι s)