@[reducible, inline]

abbrev CenterCharacter (R : Type u_1) [CommRing R] (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra R 𝔤] : Type (max (max u_1 u_2) u_1)

structure IsInHCThetaOne {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) (θ : CenterCharacter R 𝔤) : Prop

• isHC : IsHarishChandraBimodule M
• right_annihilated (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (m : M.carrier) : (M.rightAction (MulOpposite.op ↑z)) m = θ z • m

structure HCThetaOneHom {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (M₁ : LieBimodule R 𝔤) (M₂ : LieBimodule R 𝔤) (θ : CenterCharacter R 𝔤) (hM₁ : IsInHCThetaOne M₁ θ) (hM₂ : IsInHCThetaOne M₂ θ) : Type (max u_1 u_2)

• toLinearMap : M₁.carrier →ₗ[R] M₂.carrier
• left_compat (u : UniversalEnvelopingAlgebra R 𝔤) (m : M₁.carrier) : self.toLinearMap ((M₁.leftAction u) m) = (M₂.leftAction u) (self.toLinearMap m)
• right_compat (u : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (m : M₁.carrier) : self.toLinearMap ((M₁.rightAction u) m) = (M₂.rightAction u) (self.toLinearMap m)

def IsProjectiveInHCThetaOne {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (P : LieBimodule R 𝔤) (θ : CenterCharacter R 𝔤) (hP : IsInHCThetaOne P θ) : Prop

def IsTensorProductBimoduleWithUTheta {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (P : LieBimodule R 𝔤) (θ : CenterCharacter R 𝔤) (V : Type u_1) [AddCommGroup V] [Module R V] : Prop

theorem tensor_hom_bimodule_extension {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (T : LieBimodule R 𝔤) (V : Type u_1) [AddCommGroup V] [Module R V] (ι : V →ₗ[R] T.carrier) (h_gen : ∀ (t : T.carrier), ∃ (n : ℕ) (vs : Fin n → V) (us : Fin n → (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ), t = ∑ i : Fin n, (T.rightAction (us i)) (ι (vs i))) (h_central : ∀ (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (t : T.carrier), (T.rightAction (MulOpposite.op ↑z)) t = θ z • t) (Y : LieBimodule R 𝔤) (hY : IsInHCThetaOne Y θ) (ψ : V →ₗ[R] Y.carrier) : ∃ (ext_map : T.carrier →ₗ[R] Y.carrier), (∀ (v : V), ext_map (ι v) = ψ v) ∧ (∀ (u : UniversalEnvelopingAlgebra R 𝔤) (t : T.carrier), ext_map ((T.leftAction u) t) = (Y.leftAction u) (ext_map t)) ∧ ∀ (u : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (t : T.carrier), ext_map ((T.rightAction u) t) = (Y.rightAction u) (ext_map t)

theorem tensor_hom_bimodule_uniqueness {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (T : LieBimodule R 𝔤) (V : Type u_1) [AddCommGroup V] [Module R V] (ι : V →ₗ[R] T.carrier) (h_gen : ∀ (t : T.carrier), ∃ (n : ℕ) (vs : Fin n → V) (us : Fin n → (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ), t = ∑ i : Fin n, (T.rightAction (us i)) (ι (vs i))) (Y : LieBimodule R 𝔤) (f₁ f₂ : T.carrier →ₗ[R] Y.carrier) (h_f₁_right : ∀ (u : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (t : T.carrier), f₁ ((T.rightAction u) t) = (Y.rightAction u) (f₁ t)) (h_f₂_right : ∀ (u : (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ) (t : T.carrier), f₂ ((T.rightAction u) t) = (Y.rightAction u) (f₂ t)) (h_agree_on_V : ∀ (v : V), f₁ (ι v) = f₂ (ι v)) (t : T.carrier) : f₁ t = f₂ t

theorem tensor_hom_adjunction_lift {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (P : LieBimodule R 𝔤) (hP : IsInHCThetaOne P θ) (V : Type u_1) [AddCommGroup V] [Module R V] (hTV : IsTensorProductBimoduleWithUTheta P θ V) (Y₁ Y₂ : LieBimodule R 𝔤) (hY₁ : IsInHCThetaOne Y₁ θ) (hY₂ : IsInHCThetaOne Y₂ θ) (g : HCThetaOneHom Y₁ Y₂ θ hY₁ hY₂) (hg_surj : Function.Surjective ⇑g.toLinearMap) (f : HCThetaOneHom P Y₂ θ hP hY₂) (h_lin_lift : ∀ (φ : V →ₗ[R] Y₂.carrier), ∃ (ψ : V →ₗ[R] Y₁.carrier), ∀ (v : V), g.toLinearMap (ψ v) = φ v) : ∃ (lift : HCThetaOneHom P Y₁ θ hP hY₁), ∀ (m : P.carrier), g.toLinearMap (lift.toLinearMap m) = f.toLinearMap m

theorem weyl_ad_split_for_hc {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (Y₁ Y₂ : LieBimodule R 𝔤) (hY₁ : IsInHCThetaOne Y₁ θ) (hY₂ : IsInHCThetaOne Y₂ θ) (g : HCThetaOneHom Y₁ Y₂ θ hY₁ hY₂) (hg_surj : Function.Surjective ⇑g.toLinearMap) : ∃ (s : Y₂.carrier →ₗ[R] Y₁.carrier), ∀ (y₂ : Y₂.carrier), g.toLinearMap (s y₂) = y₂

theorem weyl_ad_lift_for_hc {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (Y₁ Y₂ : LieBimodule R 𝔤) (hY₁ : IsInHCThetaOne Y₁ θ) (hY₂ : IsInHCThetaOne Y₂ θ) (g : HCThetaOneHom Y₁ Y₂ θ hY₁ hY₂) (hg_surj : Function.Surjective ⇑g.toLinearMap) (V : Type u_1) [AddCommGroup V] [Module R V] (φ : V →ₗ[R] Y₂.carrier) : ∃ (ψ : V →ₗ[R] Y₁.carrier), ∀ (v : V), g.toLinearMap (ψ v) = φ v

theorem tensor_bimodule_is_projective_in_hc_theta_one {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (P : LieBimodule R 𝔤) (hP : IsInHCThetaOne P θ) (V : Type u_1) [AddCommGroup V] [Module R V] (hTV : IsTensorProductBimoduleWithUTheta P θ V) : IsProjectiveInHCThetaOne P θ hP

theorem hc_theta_one_finitely_generated_bimodule {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (Y : LieBimodule R 𝔤) (hY : IsInHCThetaOne Y θ) : ∃ (n : ℕ) (gens : Fin n → Y.carrier), ∀ (y : Y.carrier), ∃ (k : ℕ) (coeffIdx : Fin k → Fin n) (us : Fin k → (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ), y = ∑ j : Fin k, (Y.rightAction (us j)) (gens (coeffIdx j))

theorem hc_theta_one_has_ad_stable_generating_submodule {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (Y : LieBimodule R 𝔤) (hY : IsInHCThetaOne Y θ) : ∃ (V : Type u_mod) (x : AddCommGroup V) (x_1 : Module R V) (_ : Module.Finite R V) (ι : V →ₗ[R] Y.carrier), ∀ (y : Y.carrier), ∃ (n : ℕ) (vs : Fin n → V) (us : Fin n → (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ), y = ∑ i : Fin n, (Y.rightAction (us i)) (ι (vs i))

theorem tensor_product_bimodule_surjects_from_generators {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (Y : LieBimodule R 𝔤) (hY : IsInHCThetaOne Y θ) (V : Type u_mod) [AddCommGroup V] [Module R V] (ι : V →ₗ[R] Y.carrier) (h_gen : ∀ (y : Y.carrier), ∃ (n : ℕ) (vs : Fin n → V) (us : Fin n → (UniversalEnvelopingAlgebra R 𝔤)ᵐᵒᵖ), y = ∑ i : Fin n, (Y.rightAction (us i)) (ι (vs i))) : ∃ (P : LieBimodule R 𝔤) (hP : IsInHCThetaOne P θ), IsTensorProductBimoduleWithUTheta P θ V ∧ ∃ (π : HCThetaOneHom P Y θ hP hY), Function.Surjective ⇑π.toLinearMap

theorem hc_theta_one_tensor_bimodule_surjects {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (Y : LieBimodule R 𝔤) (hY : IsInHCThetaOne Y θ) : ∃ (P : LieBimodule R 𝔤) (hP : IsInHCThetaOne P θ) (V : Type u_mod) (x : AddCommGroup V) (x_1 : Module R V), IsTensorProductBimoduleWithUTheta P θ V ∧ ∃ (π : HCThetaOneHom P Y θ hP hY), Function.Surjective ⇑π.toLinearMap

theorem hc_theta_one_enough_projectives {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] [LieAlgebra.IsSemisimple R 𝔤] [Module.Finite R 𝔤] (θ : CenterCharacter R 𝔤) (Y : LieBimodule R 𝔤) (hY : IsInHCThetaOne Y θ) : ∃ (P : LieBimodule R 𝔤) (hP : IsInHCThetaOne P θ), IsProjectiveInHCThetaOne P θ hP ∧ ∃ (π : HCThetaOneHom P Y θ hP hY), Function.Surjective ⇑π.toLinearMap

def LieBimodule.IsFiniteLengthBimodule {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) : Prop

def iteratedKerThetaRightAction {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) (θ : CenterCharacter R 𝔤) (zs : List ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))) (m : M.carrier) : M.carrier

structure IsInHCTheta {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) (θ : CenterCharacter R 𝔤) : Prop

• isHC : IsHarishChandraBimodule M
• annihilated_by_power : ∃ (n : ℕ), ∀ (zs : List ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R 𝔤))), zs.length = n → ∀ (m : M.carrier), iteratedKerThetaRightAction M θ zs m = 0

def IsInHC {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (M : LieBimodule R 𝔤) : Prop

def LieBimodule.AreIsomorphic {R : Type u_R} [CommRing R] {𝔤 : Type u_𝔤} [LieRing 𝔤] [LieAlgebra R 𝔤] (M₁ : LieBimodule R 𝔤) (M₂ : LieBimodule R 𝔤) : Prop

def HasFinitelyManySimpleBimodules {𝔤 : Type u_𝔤''} [LieRing 𝔤] [LieAlgebra ℂ 𝔤] (θ : CenterCharacter ℂ 𝔤) : Prop

theorem theorem_25_6_and_proposition_16_2 {𝔤'' : Type u_𝔤''} [LieRing 𝔤''] [LieAlgebra ℂ 𝔤''] [LieAlgebra.IsSemisimple ℂ 𝔤''] [Module.Finite ℂ 𝔤''] (θ : CenterCharacter ℂ 𝔤'') (Y : LieBimodule ℂ 𝔤'') (hY : IsInHCThetaOne Y θ) : Y.IsFiniteLengthBimodule

theorem hc_theta_filtration_reduction_step {𝔤'' : Type u_𝔤''} [LieRing 𝔤''] [LieAlgebra ℂ 𝔤''] [LieAlgebra.IsSemisimple ℂ 𝔤''] [Module.Finite ℂ 𝔤''] (θ₀ : CenterCharacter ℂ 𝔤'') (Y₀ : LieBimodule ℂ 𝔤'') (hY₀_hc : IsHarishChandraBimodule Y₀) (n : ℕ) (h_annihilation : ∀ (zs : List ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤''))), zs.length = n + 1 → ∀ (m : Y₀.carrier), iteratedKerThetaRightAction Y₀ θ₀ zs m = 0) (h_hc1_fl : ∀ (Z : LieBimodule ℂ 𝔤''), IsInHCThetaOne Z θ₀ → Z.IsFiniteLengthBimodule) (h_lower_fl : ∀ (Z : LieBimodule ℂ 𝔤''), IsHarishChandraBimodule Z → (∀ (zs : List ↥(Subalgebra.center ℂ (UniversalEnvelopingAlgebra ℂ 𝔤''))), zs.length = n → ∀ (m : Z.carrier), iteratedKerThetaRightAction Z θ₀ zs m = 0) → Z.IsFiniteLengthBimodule) : Y₀.IsFiniteLengthBimodule

theorem hc_theta_filtration_finite_length {𝔤'' : Type u_𝔤''} [LieRing 𝔤''] [LieAlgebra ℂ 𝔤''] [LieAlgebra.IsSemisimple ℂ 𝔤''] [Module.Finite ℂ 𝔤''] (θ : CenterCharacter ℂ 𝔤'') (Y : LieBimodule ℂ 𝔤'') (hY : IsInHCTheta Y θ) (h_hc1_fl : ∀ (Z : LieBimodule ℂ 𝔤''), IsInHCThetaOne Z θ → Z.IsFiniteLengthBimodule) : Y.IsFiniteLengthBimodule

theorem hc_block_decomposition_step {𝔤'' : Type u_𝔤''} [LieRing 𝔤''] [LieAlgebra ℂ 𝔤''] [LieAlgebra.IsSemisimple ℂ 𝔤''] [Module.Finite ℂ 𝔤''] (Y₀ : LieBimodule ℂ 𝔤'') (hY₀ : IsInHC Y₀) (h_hc_theta_fl : ∀ (θ₀ : CenterCharacter ℂ 𝔤'') (Z : LieBimodule ℂ 𝔤''), IsInHCTheta Z θ₀ → Z.IsFiniteLengthBimodule) : Y₀.IsFiniteLengthBimodule

theorem corollary_25_7 {𝔤'' : Type u_𝔤''} [LieRing 𝔤''] [LieAlgebra ℂ 𝔤''] [LieAlgebra.IsSemisimple ℂ 𝔤''] [Module.Finite ℂ 𝔤''] (θ : CenterCharacter ℂ 𝔤'') (Y : LieBimodule ℂ 𝔤'') (hY : IsInHCThetaOne Y θ) : Y.IsFiniteLengthBimodule

theorem corollary_25_7_hc_theta {𝔤'' : Type u_𝔤''} [LieRing 𝔤''] [LieAlgebra ℂ 𝔤''] [LieAlgebra.IsSemisimple ℂ 𝔤''] [Module.Finite ℂ 𝔤''] (θ : CenterCharacter ℂ 𝔤'') (Y : LieBimodule ℂ 𝔤'') (hY : IsInHCTheta Y θ) : Y.IsFiniteLengthBimodule

theorem corollary_25_7_hc {𝔤'' : Type u_𝔤''} [LieRing 𝔤''] [LieAlgebra ℂ 𝔤''] [LieAlgebra.IsSemisimple ℂ 𝔤''] [Module.Finite ℂ 𝔤''] (Y : LieBimodule ℂ 𝔤'') (hY : IsInHC Y) : Y.IsFiniteLengthBimodule