structure LieModuleObj (R : Type u_R) [CommRing R] (g : Type u_g) [LieRing g] [LieAlgebra R g] : Type (max (max u_R u_g) (u_mod + 1))

• carrier : Type u_mod
• instAddCommGroup : AddCommGroup self.carrier
• instModule : Module R self.carrier
• instLieRingModule : LieRingModule g self.carrier
• instLieModule : LieModule R g self.carrier

def IsRegularWeight {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} {rd : PositiveRootData D} (wg : WeylGroupData D) (cd : RootCorootData rd) (lam : ↥D.𝔥 →ₗ[R] R) : Prop

structure LieModuleMor (R : Type u_R) [CommRing R] (g : Type u_g) [LieRing g] [LieAlgebra R g] (X Y : LieModuleObj R g) : Type u_mod

• toLinearMap : X.carrier →ₗ[R] Y.carrier
• lie_compat (x : g) (m : X.carrier) : self.toLinearMap ⁅x, m⁆ = ⁅x, self.toLinearMap m⁆

structure LieModuleIso (R : Type u_R) [CommRing R] (g : Type u_g) [LieRing g] [LieAlgebra R g] (X Y : LieModuleObj R g) : Type u_mod

• forward : LieModuleMor R g X Y
• backward : LieModuleMor R g Y X
• left_inv (m : X.carrier) : self.backward.toLinearMap (self.forward.toLinearMap m) = m
• right_inv (m : Y.carrier) : self.forward.toLinearMap (self.backward.toLinearMap m) = m

structure TlambdaData {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) : Type (max (max u_R u_g) (u_mod + 1))

• applyObj (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta) : LieModuleObj R g
• applyHom {Y₁ Y₂ : LieBimodule R g} {hY₁ : IsInHCThetaOne Y₁ theta} {hY₂ : IsInHCThetaOne Y₂ theta} : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂ → LieModuleMor R g (self.applyObj Y₁ hY₁) (self.applyObj Y₂ hY₂)
• applyHom_comp {Y₁ Y₂ Y₃ : LieBimodule R g} {hY₁ : IsInHCThetaOne Y₁ theta} {hY₂ : IsInHCThetaOne Y₂ theta} {hY₃ : IsInHCThetaOne Y₃ theta} (g' : HCThetaOneHom Y₂ Y₃ theta hY₂ hY₃) (f : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) (comp_gf : HCThetaOneHom Y₁ Y₃ theta hY₁ hY₃) : comp_gf.toLinearMap = g'.toLinearMap ∘ₗ f.toLinearMap → (self.applyHom comp_gf).toLinearMap = (self.applyHom g').toLinearMap ∘ₗ (self.applyHom f).toLinearMap
• applyHom_id {Y : LieBimodule R g} {hY : IsInHCThetaOne Y theta} (idY : HCThetaOneHom Y Y theta hY hY) : idY.toLinearMap = LinearMap.id → (self.applyHom idY).toLinearMap = LinearMap.id
• applyHom_surjective {Y₁ Y₂ : LieBimodule R g} {hY₁ : IsInHCThetaOne Y₁ theta} {hY₂ : IsInHCThetaOne Y₂ theta} (f : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) : Function.Surjective ⇑f.toLinearMap → Function.Surjective ⇑(self.applyHom f).toLinearMap
• applyHom_exact {Y₁ Y₂ Y₃ : LieBimodule R g} {hY₁ : IsInHCThetaOne Y₁ theta} {hY₂ : IsInHCThetaOne Y₂ theta} {hY₃ : IsInHCThetaOne Y₃ theta} (p₁ : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) (p₀ : HCThetaOneHom Y₂ Y₃ theta hY₂ hY₃) : Function.Exact ⇑p₁.toLinearMap ⇑p₀.toLinearMap → Function.Surjective ⇑p₀.toLinearMap → Function.Exact ⇑(self.applyHom p₁).toLinearMap ⇑(self.applyHom p₀).toLinearMap
• applyObj_isCategoryO {D : TriangularDecomposition R g} {rd : PositiveRootData D} (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta) : IsCategoryO D rd (self.applyObj Y hY).carrier

structure HlambdaData {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) : Type (max (max u_R u_g) (u_mod + 1))

• applyObj (X : LieModuleObj R g) : LieBimodule R g
• inHCThetaOne (X : LieModuleObj R g) : IsInHCThetaOne (self.applyObj X) theta

structure IsInBlock_LambdaPlusP {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} (rd : PositiveRootData D) (X : LieModuleObj R g) (theta : CenterCharacter R g) : Prop

• inCategoryO : IsCategoryO D rd X.carrier
• existsUEAAction : ∃ (ueaAct : UniversalEnvelopingAlgebra R g →ₐ[R] Module.End R X.carrier), GeneralizedEigenspaceCenter X.carrier ueaAct theta = ⊤

def IsInO_Lambda {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} (rd : PositiveRootData D) (theta : CenterCharacter R g) (Tl : TlambdaData theta) (X : LieModuleObj R g) : Prop

theorem proposition_25_10 {ObjA : Type u_1} {ObjB : Type u_2} (HomA : ObjA → ObjA → Type u_3) (HomB : ObjB → ObjB → Type u_4) (T_obj : ObjA → ObjB) (T_map : {X Y : ObjA} → HomA X Y → HomB (T_obj X) (T_obj Y)) (IsProjA : ObjA → Prop) (_IsProjB : ObjB → Prop) (compA : {X Y Z : ObjA} → HomA Y Z → HomA X Y → HomA X Z) (compB : {X Y Z : ObjB} → HomB Y Z → HomB X Y → HomB X Z) (_T_functorial : ∀ {X Y Z : ObjA} (g : HomA Y Z) (f : HomA X Y), T_map (compA g f) = compB (T_map g) (T_map f)) (idA : (X : ObjA) → HomA X X) (idB : (X : ObjB) → HomB X X) (_T_preserves_id : ∀ (X : ObjA), T_map (idA X) = idB (T_obj X)) (IsPresentationA : {P₁ P₀ X : ObjA} → HomA P₁ P₀ → HomA P₀ X → Prop) (IsPresentationB : {Q₁ Q₀ Y : ObjB} → HomB Q₁ Q₀ → HomB Q₀ Y → Prop) (_enough_proj : ∀ (X : ObjA), ∃ (P₀ : ObjA) (P₁ : ObjA), IsProjA P₀ ∧ IsProjA P₁ ∧ ∃ (p₁ : HomA P₁ P₀) (p₀ : HomA P₀ X), IsPresentationA p₁ p₀) (_T_preserves_proj : ∀ (P : ObjA), IsProjA P → _IsProjB (T_obj P)) (_T_right_exact : ∀ {P₁ P₀ X : ObjA} (p₁ : HomA P₁ P₀) (p₀ : HomA P₀ X), IsPresentationA p₁ p₀ → IsPresentationB (T_map p₁) (T_map p₀)) (_T_ff_on_proj : ∀ (P₀ P₁ : ObjA), IsProjA P₀ → IsProjA P₁ → Function.Bijective fun (f : HomA P₁ P₀) => T_map f) (IsIsoB : {Y₁ Y₂ : ObjB} → HomB Y₁ Y₂ → Prop) (_lift_through_pres : ∀ {P₁ P₀ X P₁' P₀' X' : ObjA} (p₁ : HomA P₁ P₀) (p₀ : HomA P₀ X) (p₁' : HomA P₁' P₀') (p₀' : HomA P₀' X'), IsPresentationA p₁ p₀ → IsPresentationA p₁' p₀' → IsProjA P₀ → IsProjA P₁ → ∀ (a : HomA X X'), ∃ (a₀ : HomA P₀ P₀') (a₁ : HomA P₁ P₁'), compA p₀' a₀ = compA a p₀ ∧ compA a₀ p₁ = compA p₁' a₁) (_lift_through_presB : ∀ {Q₁ Q₀ Y Q₁' Q₀' Y' : ObjB} (q₁ : HomB Q₁ Q₀) (q₀ : HomB Q₀ Y) (q₁' : HomB Q₁' Q₀') (q₀' : HomB Q₀' Y'), IsPresentationB q₁ q₀ → IsPresentationB q₁' q₀' → _IsProjB Q₀ → _IsProjB Q₁ → ∀ (b : HomB Y Y'), ∃ (b₀ : HomB Q₀ Q₀') (b₁ : HomB Q₁ Q₁'), compB q₀' b₀ = compB b q₀ ∧ compB b₀ q₁ = compB q₁' b₁) (_pres_epi : ∀ {P₁ P₀ X : ObjA} (p₁ : HomA P₁ P₀) (p₀ : HomA P₀ X), IsPresentationA p₁ p₀ → ∀ {Y : ObjA} (f g : HomA X Y), compA f p₀ = compA g p₀ → f = g) (_presB_epi : ∀ {Q₁ Q₀ Y : ObjB} (q₁ : HomB Q₁ Q₀) (q₀ : HomB Q₀ Y), IsPresentationB q₁ q₀ → ∀ {Z : ObjB} (f g : HomB Y Z), compB f q₀ = compB g q₀ → f = g) (_five_lemma_inj : ∀ {P₁ P₀ X Q₁ Q₀ Y : ObjA} (p₁ : HomA P₁ P₀) (p₀ : HomA P₀ X) (q₁ : HomA Q₁ Q₀) (q₀ : HomA Q₀ Y), IsPresentationA p₁ p₀ → IsPresentationA q₁ q₀ → IsProjA P₀ → IsProjA P₁ → IsProjA Q₀ → IsProjA Q₁ → ∀ (a₀ a₀' : HomA P₀ Q₀), compB (T_map q₀) (T_map a₀) = compB (T_map q₀) (T_map a₀') → a₀ = a₀') (_descent_through_pres : ∀ {P₁ P₀ X P₁' P₀' X' : ObjA} (p₁ : HomA P₁ P₀) (p₀ : HomA P₀ X) (p₁' : HomA P₁' P₀') (p₀' : HomA P₀' X'), IsPresentationA p₁ p₀ → IsPresentationA p₁' p₀' → ∀ (a₀ : HomA P₀ P₀') (a₁ : HomA P₁ P₁'), compA a₀ p₁ = compA p₁' a₁ → ∃ (a : HomA X X'), compA p₀' a₀ = compA a p₀) (_cokernel_in_image : ∀ {P₁ P₀ : ObjA} (g : HomA P₁ P₀), IsProjA P₀ → IsProjA P₁ → ∀ (Y : ObjB) (f₀ : HomB (T_obj P₀) Y), IsPresentationB (T_map g) f₀ → ∃ (X : ObjA) (iso : HomB (T_obj X) Y), IsIsoB iso) : (∀ (X Y : ObjA), Function.Bijective fun (f : HomA X Y) => T_map f) ∧ (∀ (X : ObjA), ∃ (P₀ : ObjA) (P₁ : ObjA), IsProjA P₀ ∧ IsProjA P₁ ∧ ∃ (f₁ : HomB (T_obj P₁) (T_obj P₀)) (f₀ : HomB (T_obj P₀) (T_obj X)), IsPresentationB f₁ f₀) ∧ ∀ (Y : ObjB) (P₀ P₁ : ObjA) (f₁ : HomB (T_obj P₁) (T_obj P₀)) (f₀ : HomB (T_obj P₀) Y), IsProjA P₀ → IsProjA P₁ → IsPresentationB f₁ f₀ → ∃ (X : ObjA) (iso : HomB (T_obj X) Y), IsIsoB iso

def VermaCarrier {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (D : TriangularDecomposition R g) (wt : ↥D.𝔥 →ₗ[R] R) : Type u_mod

@[implicit_reducible]

noncomputable instance VermaCarrier.instACG {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (D : TriangularDecomposition R g) (wt : ↥D.𝔥 →ₗ[R] R) : AddCommGroup (VermaCarrier D wt)

@[implicit_reducible]

noncomputable instance VermaCarrier.instMod {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (D : TriangularDecomposition R g) (wt : ↥D.𝔥 →ₗ[R] R) : Module R (VermaCarrier D wt)

@[implicit_reducible]

noncomputable instance VermaCarrier.instLRM {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (D : TriangularDecomposition R g) (wt : ↥D.𝔥 →ₗ[R] R) : LieRingModule g (VermaCarrier D wt)

instance VermaCarrier.instLM {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (D : TriangularDecomposition R g) (wt : ↥D.𝔥 →ₗ[R] R) : LieModule R g (VermaCarrier D wt)

@[reducible]

def LieBimodule.instLieRingModuleOfLeftAction {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (Y : LieBimodule R g) : LieRingModule g Y.carrier

@[reducible]

def LieBimodule.instLieModuleOfLeftAction {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (Y : LieBimodule R g) : LieModule R g Y.carrier

noncomputable def Tlambda_exists {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} {rd : PositiveRootData D} (wg : WeylGroupData D) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd wg lam) : TlambdaData theta

theorem vermaCarrier_central_character {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} (wg : WeylGroupData D) (wt : ↥D.𝔥 →ₗ[R] R) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R g))) (m : VermaCarrier D wt) : (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R g (VermaCarrier D wt))) ↑z) m = (evalHC D wg (wt + wg.ρ)) z • m

theorem homFinBimodule_vermaCarrier_isHC {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [Module.Finite R g] {D : TriangularDecomposition R g} (wt : ↥D.𝔥 →ₗ[R] R) (N : Type u_mod) [AddCommGroup N] [Module R N] [LieRingModule g N] [LieModule R g N] : IsHarishChandraBimodule (HomFinBimodule (VermaCarrier D wt) N)

theorem homFinBimodule_right_character {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [Module.Finite R g] {D : TriangularDecomposition R g} (wg : WeylGroupData D) (wt : ↥D.𝔥 →ₗ[R] R) (X : LieModuleObj R g) (z : ↥(Subalgebra.center R (UniversalEnvelopingAlgebra R g))) (m : (HomFinBimodule (VermaCarrier D wt) X.carrier).carrier) : ((HomFinBimodule (VermaCarrier D wt) X.carrier).rightAction (MulOpposite.op ↑z)) m = (evalHC D wg (wt + wg.ρ)) z • m

noncomputable def Hlambda_exists {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} [Module.Finite R g] {rd : PositiveRootData D} (wg : WeylGroupData D) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd wg lam) (htheta : theta = evalHC D wg lam) : HlambdaData theta

@[reducible, inline]

abbrev HCThetaOneObj (R : Type u_R) [CommRing R] (g : Type u_g) [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) : Type (max 0 (max u_R u_g) (u_mod + 1))

def HCThetaOneHomBundled {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) (A B : HCThetaOneObj R g theta) : Type u_mod

def TlambdaObjBundled {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (A : HCThetaOneObj R g theta) : LieModuleObj R g

def TlambdaMapBundled {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {A B : HCThetaOneObj R g theta} (f : HCThetaOneHomBundled theta A B) : LieModuleMor R g (TlambdaObjBundled Tl A) (TlambdaObjBundled Tl B)

def IsProjHCBundled {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) (A : HCThetaOneObj R g theta) : Prop

noncomputable def HCThetaOne_comp {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} {A B C : HCThetaOneObj R g theta} : HCThetaOneHomBundled theta B C → HCThetaOneHomBundled theta A B → HCThetaOneHomBundled theta A C

def LieModuleMor_comp {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {X Y Z : LieModuleObj R g} (g' : LieModuleMor R g Y Z) (f : LieModuleMor R g X Y) : LieModuleMor R g X Z

def LieModuleMor_sub {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {X Y : LieModuleObj R g} (f g' : LieModuleMor R g X Y) : LieModuleMor R g X Y

noncomputable def HCThetaOne_id {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (A : HCThetaOneObj R g theta) : HCThetaOneHomBundled theta A A

def LieModuleMor_id {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (X : LieModuleObj R g) : LieModuleMor R g X X

def IsPresentationHC {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} {P₁ P₀ X : HCThetaOneObj R g theta} (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X) : Prop

def IsPresentationO {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {Q₁ Q₀ Y : LieModuleObj R g} (q₁ : LieModuleMor R g Q₁ Q₀) (q₀ : LieModuleMor R g Q₀ Y) : Prop

def IsProjO {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (P : LieModuleObj R g) : Prop

def IsIsoO {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {Y₁ Y₂ : LieModuleObj R g} (f : LieModuleMor R g Y₁ Y₂) : Prop

theorem LieModuleMor.ext' {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {X Y : LieModuleObj R g} {f g' : LieModuleMor R g X Y} (h : f.toLinearMap = g'.toLinearMap) : f = g'

theorem Tlambda_functorial {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {A B C : HCThetaOneObj R g theta} (g' : HCThetaOneHomBundled theta B C) (f : HCThetaOneHomBundled theta A B) : TlambdaMapBundled Tl (HCThetaOne_comp g' f) = LieModuleMor_comp (TlambdaMapBundled Tl g') (TlambdaMapBundled Tl f)

theorem Tlambda_preserves_id {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (A : HCThetaOneObj R g theta) : TlambdaMapBundled Tl (HCThetaOne_id A) = LieModuleMor_id (TlambdaObjBundled Tl A)

theorem HCThetaOne_enough_proj_cover {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] {theta : CenterCharacter R g} (X : HCThetaOneObj R g theta) : ∃ (P : HCThetaOneObj R g theta), IsProjHCBundled theta P ∧ ∃ (π : HCThetaOneHomBundled theta P X), Function.Surjective ⇑π.toLinearMap

theorem HCThetaOne_kernel_in_category {R : Type u_R} [CommRing R] [IsNoetherianRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} {P₀ X : HCThetaOneObj R g theta} (p₀ : HCThetaOneHomBundled theta P₀ X) : ∃ (K : HCThetaOneObj R g theta) (ι : HCThetaOneHomBundled theta K P₀), Function.Injective ⇑ι.toLinearMap ∧ (∀ (m : (↑K).carrier), p₀.toLinearMap (ι.toLinearMap m) = 0) ∧ ∀ (m : (↑P₀).carrier), p₀.toLinearMap m = 0 → ∃ (n : (↑K).carrier), ι.toLinearMap n = m

theorem HCThetaOne_enough_proj {R : Type u_R} [CommRing R] [IsNoetherianRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] {theta : CenterCharacter R g} (X : HCThetaOneObj R g theta) : ∃ (P₀ : HCThetaOneObj R g theta) (P₁ : HCThetaOneObj R g theta), IsProjHCBundled theta P₀ ∧ IsProjHCBundled theta P₁ ∧ ∃ (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X), IsPresentationHC p₁ p₀

noncomputable def Hlambda_applyObj_bundled {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (X : LieModuleObj R g) : HCThetaOneObj R g theta

noncomputable def Hlambda_applyHom_bundled {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {X Y : LieModuleObj R g} (f : LieModuleMor R g X Y) : HCThetaOneHomBundled theta (Hlambda_applyObj_bundled Tl X) (Hlambda_applyObj_bundled Tl Y)

theorem Hlambda_preserves_surjective {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {X Y : LieModuleObj R g} (f : LieModuleMor R g X Y) (hf_surj : Function.Surjective ⇑f.toLinearMap) : Function.Surjective ⇑(Hlambda_applyHom_bundled Tl f).toLinearMap

noncomputable def adjunction_forward {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (P : HCThetaOneObj R g theta) {Y : LieModuleObj R g} (f : LieModuleMor R g (TlambdaObjBundled Tl P) Y) : HCThetaOneHomBundled theta P (Hlambda_applyObj_bundled Tl Y)

theorem adjunction_backward_lift {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (P : HCThetaOneObj R g theta) {Y₁ Y₂ : LieModuleObj R g} (g' : LieModuleMor R g Y₁ Y₂) (f : LieModuleMor R g (TlambdaObjBundled Tl P) Y₂) (χ : HCThetaOneHomBundled theta P (Hlambda_applyObj_bundled Tl Y₁)) (hχ : ∀ (m : (↑P).carrier), (Hlambda_applyHom_bundled Tl g').toLinearMap (χ.toLinearMap m) = (adjunction_forward Tl P f).toLinearMap m) : ∃ (f' : LieModuleMor R g (TlambdaObjBundled Tl P) Y₁), ∀ (m : (TlambdaObjBundled Tl P).carrier), g'.toLinearMap (f'.toLinearMap m) = f.toLinearMap m

theorem adjunction_Hlambda_lifting {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (P : HCThetaOneObj R g theta) {Y₁ Y₂ : LieModuleObj R g} (g' : LieModuleMor R g Y₁ Y₂) (f : LieModuleMor R g (TlambdaObjBundled Tl P) Y₂) (hg_surj : Function.Surjective ⇑g'.toLinearMap) : ∃ (A₁ : HCThetaOneObj R g theta) (A₂ : HCThetaOneObj R g theta) (φ : HCThetaOneHomBundled theta A₁ A₂) (ψ : HCThetaOneHomBundled theta P A₂), Function.Surjective ⇑φ.toLinearMap ∧ ∀ (χ : HCThetaOneHomBundled theta P A₁), (∀ (m : (↑P).carrier), φ.toLinearMap (χ.toLinearMap m) = ψ.toLinearMap m) → ∃ (f' : LieModuleMor R g (TlambdaObjBundled Tl P) Y₁), ∀ (m : (TlambdaObjBundled Tl P).carrier), g'.toLinearMap (f'.toLinearMap m) = f.toLinearMap m

theorem Tlambda_preserves_proj {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (P : HCThetaOneObj R g theta) : IsProjHCBundled theta P → IsProjO (TlambdaObjBundled Tl P)

theorem Tlambda_right_exact {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {P₁ P₀ X : HCThetaOneObj R g theta} (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X) : IsPresentationHC p₁ p₀ → IsPresentationO (TlambdaMapBundled Tl p₁) (TlambdaMapBundled Tl p₀)

theorem Tlambda_ff_on_proj {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) (P₀ P₁ : HCThetaOneObj R g theta) : IsProjHCBundled theta P₀ → IsProjHCBundled theta P₁ → Function.Bijective fun (f : HCThetaOneHomBundled theta P₁ P₀) => TlambdaMapBundled Tl f

theorem HCThetaOne_lift_through_pres {R : Type u_R} [CommRing R] [IsNoetherianRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} {P₁ P₀ X P₁' P₀' X' : HCThetaOneObj R g theta} (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X) (p₁' : HCThetaOneHomBundled theta P₁' P₀') (p₀' : HCThetaOneHomBundled theta P₀' X') : IsPresentationHC p₁ p₀ → IsPresentationHC p₁' p₀' → IsProjHCBundled theta P₀ → IsProjHCBundled theta P₁ → ∀ (a : HCThetaOneHomBundled theta X X'), ∃ (a₀ : HCThetaOneHomBundled theta P₀ P₀') (a₁ : HCThetaOneHomBundled theta P₁ P₁'), HCThetaOne_comp p₀' a₀ = HCThetaOne_comp a p₀ ∧ HCThetaOne_comp a₀ p₁ = HCThetaOne_comp p₁' a₁

@[implicit_reducible]

noncomputable instance LieModuleMor_ker_lieRingModule {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {X Y : LieModuleObj R g} (f : LieModuleMor R g X Y) : LieRingModule g ↥f.toLinearMap.ker

instance LieModuleMor_ker_lieModule {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {X Y : LieModuleObj R g} (f : LieModuleMor R g X Y) : LieModule R g ↥f.toLinearMap.ker

noncomputable def LieModuleMor_kerObj {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {X Y : LieModuleObj R g} (f : LieModuleMor R g X Y) : LieModuleObj R g

noncomputable def LieModuleMor_corestrToKer {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {A B C : LieModuleObj R g} (q₁ : LieModuleMor R g A B) (q₀ : LieModuleMor R g B C) (hcomp : ∀ (m : A.carrier), q₀.toLinearMap (q₁.toLinearMap m) = 0) : LieModuleMor R g A (LieModuleMor_kerObj q₀)

theorem LieModuleMor_corestrToKer_surj {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {A B C : LieModuleObj R g} (q₁ : LieModuleMor R g A B) (q₀ : LieModuleMor R g B C) (hcomp : ∀ (m : A.carrier), q₀.toLinearMap (q₁.toLinearMap m) = 0) (hexact : ∀ (m : B.carrier), q₀.toLinearMap m = 0 → ∃ (n : A.carrier), q₁.toLinearMap n = m) : Function.Surjective ⇑(LieModuleMor_corestrToKer q₁ q₀ hcomp).toLinearMap

theorem O_lift_through_pres {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {Q₁ Q₀ Y Q₁' Q₀' Y' : LieModuleObj R g} (q₁ : LieModuleMor R g Q₁ Q₀) (q₀ : LieModuleMor R g Q₀ Y) (q₁' : LieModuleMor R g Q₁' Q₀') (q₀' : LieModuleMor R g Q₀' Y') (hpres : IsPresentationO q₁ q₀) (hpres' : IsPresentationO q₁' q₀') (hproj₀ : IsProjO Q₀) (hproj₁ : IsProjO Q₁) (b : LieModuleMor R g Y Y') : ∃ (b₀ : LieModuleMor R g Q₀ Q₀') (b₁ : LieModuleMor R g Q₁ Q₁'), LieModuleMor_comp q₀' b₀ = LieModuleMor_comp b q₀ ∧ LieModuleMor_comp b₀ q₁ = LieModuleMor_comp q₁' b₁

theorem HCThetaOne_pres_epi {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} {P₁ P₀ X : HCThetaOneObj R g theta} (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X) : IsPresentationHC p₁ p₀ → ∀ {Y : HCThetaOneObj R g theta} (f g✝ : HCThetaOneHomBundled theta X Y), HCThetaOne_comp f p₀ = HCThetaOne_comp g✝ p₀ → f = g✝

theorem O_pres_epi {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {Q₁ Q₀ Y : LieModuleObj R g} (q₁ : LieModuleMor R g Q₁ Q₀) (q₀ : LieModuleMor R g Q₀ Y) : IsPresentationO q₁ q₀ → ∀ {Z : LieModuleObj R g} (f g✝ : LieModuleMor R g Y Z), LieModuleMor_comp f q₀ = LieModuleMor_comp g✝ q₀ → f = g✝

theorem Tlambda_faithful_on_projHC_ax {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {P₁ P₀ X Q₁ Q₀ Y : HCThetaOneObj R g theta} (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X) (q₁ : HCThetaOneHomBundled theta Q₁ Q₀) (q₀ : HCThetaOneHomBundled theta Q₀ Y) : IsPresentationHC p₁ p₀ → IsPresentationHC q₁ q₀ → IsProjHCBundled theta P₀ → IsProjHCBundled theta P₁ → IsProjHCBundled theta Q₀ → IsProjHCBundled theta Q₁ → ∀ (a₀ a₀' : HCThetaOneHomBundled theta P₀ Q₀), LieModuleMor_comp (TlambdaMapBundled Tl q₀) (TlambdaMapBundled Tl a₀) = LieModuleMor_comp (TlambdaMapBundled Tl q₀) (TlambdaMapBundled Tl a₀') → a₀ = a₀'

theorem Tlambda_five_lemma_inj {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {P₁ P₀ X Q₁ Q₀ Y : HCThetaOneObj R g theta} (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X) (q₁ : HCThetaOneHomBundled theta Q₁ Q₀) (q₀ : HCThetaOneHomBundled theta Q₀ Y) (hp : IsPresentationHC p₁ p₀) (hq : IsPresentationHC q₁ q₀) (hP₀ : IsProjHCBundled theta P₀) (hP₁ : IsProjHCBundled theta P₁) (hQ₀ : IsProjHCBundled theta Q₀) (hQ₁ : IsProjHCBundled theta Q₁) (a₀ a₀' : HCThetaOneHomBundled theta P₀ Q₀) : LieModuleMor_comp (TlambdaMapBundled Tl q₀) (TlambdaMapBundled Tl a₀) = LieModuleMor_comp (TlambdaMapBundled Tl q₀) (TlambdaMapBundled Tl a₀') → a₀ = a₀'

theorem HCThetaOne_descent_through_pres {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} {P₁ P₀ X P₁' P₀' X' : HCThetaOneObj R g theta} (p₁ : HCThetaOneHomBundled theta P₁ P₀) (p₀ : HCThetaOneHomBundled theta P₀ X) (p₁' : HCThetaOneHomBundled theta P₁' P₀') (p₀' : HCThetaOneHomBundled theta P₀' X') (hpres : IsPresentationHC p₁ p₀) (hpres' : IsPresentationHC p₁' p₀') (a₀ : HCThetaOneHomBundled theta P₀ P₀') (a₁ : HCThetaOneHomBundled theta P₁ P₁') : HCThetaOne_comp a₀ p₁ = HCThetaOne_comp p₁' a₁ → ∃ (a : HCThetaOneHomBundled theta X X'), HCThetaOne_comp p₀' a₀ = HCThetaOne_comp a p₀

theorem HCThetaOne_cokernel_exists {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} {P₁ P₀ : HCThetaOneObj R g theta} (g' : HCThetaOneHomBundled theta P₁ P₀) : ∃ (X : HCThetaOneObj R g theta) (p₀ : HCThetaOneHomBundled theta P₀ X), IsPresentationHC g' p₀

theorem O_cokernel_unique_iso {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {Q₁ Q₀ Z₁ Z₂ : LieModuleObj R g} (q₁ : LieModuleMor R g Q₁ Q₀) (q₀ : LieModuleMor R g Q₀ Z₁) (f₀ : LieModuleMor R g Q₀ Z₂) (hpres₁ : IsPresentationO q₁ q₀) (hpres₂ : IsPresentationO q₁ f₀) : ∃ (iso : LieModuleMor R g Z₁ Z₂), IsIsoO iso

theorem O_cokernel_in_image {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {theta : CenterCharacter R g} (Tl : TlambdaData theta) {P₁ P₀ : HCThetaOneObj R g theta} (g' : HCThetaOneHomBundled theta P₁ P₀) : IsProjHCBundled theta P₀ → IsProjHCBundled theta P₁ → ∀ (Y : LieModuleObj R g) (f₀ : LieModuleMor R g (TlambdaObjBundled Tl P₀) Y), IsPresentationO (TlambdaMapBundled Tl g') f₀ → ∃ (X : HCThetaOneObj R g theta) (iso : LieModuleMor R g (TlambdaObjBundled Tl X) Y), IsIsoO iso

theorem Tlambda_prop_25_10_application {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [IsNoetherianRing R] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] {D : TriangularDecomposition R g} {rd : PositiveRootData D} (_wg : WeylGroupData D) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd _wg lam) (Tl : TlambdaData theta) (Y₁ Y₂ : LieBimodule R g) (hY₁ : IsInHCThetaOne Y₁ theta) (hY₂ : IsInHCThetaOne Y₂ theta) : Function.Bijective fun (f : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) => Tl.applyHom f

noncomputable def adjunction_unit_Tl_iso {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) (Tl : TlambdaData theta) (Hl : HlambdaData theta) (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta) : LieModuleIso R g (Tl.applyObj Y hY) (Tl.applyObj (Hl.applyObj (Tl.applyObj Y hY)) ⋯)

theorem adjunction_unit_iso_of_fully_faithful {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) (Tl : TlambdaData theta) (Hl : HlambdaData theta) (hff : ∀ (Y₁ Y₂ : LieBimodule R g) (hY₁ : IsInHCThetaOne Y₁ theta) (hY₂ : IsInHCThetaOne Y₂ theta), Function.Bijective fun (f : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) => Tl.applyHom f) (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta) : ∃ (isoF : HCThetaOneHom Y (Hl.applyObj (Tl.applyObj Y hY)) theta hY ⋯) (isoB : HCThetaOneHom (Hl.applyObj (Tl.applyObj Y hY)) Y theta ⋯ hY), (∀ (m : Y.carrier), isoB.toLinearMap (isoF.toLinearMap m) = m) ∧ ∀ (m : (Hl.applyObj (Tl.applyObj Y hY)).carrier), isoF.toLinearMap (isoB.toLinearMap m) = m

theorem Tlambda_unit_isomorphism {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [IsNoetherianRing R] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] {D : TriangularDecomposition R g} {rd : PositiveRootData D} (_wg : WeylGroupData D) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd _wg lam) (Tl : TlambdaData theta) (Hl : HlambdaData theta) (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta) : have TlY := Tl.applyObj Y hY; let HlTlY := Hl.applyObj TlY; have hHlTlY := ⋯; ∃ (isoF : HCThetaOneHom Y HlTlY theta hY hHlTlY) (isoB : HCThetaOneHom HlTlY Y theta hHlTlY hY), (∀ (m : Y.carrier), isoB.toLinearMap (isoF.toLinearMap m) = m) ∧ ∀ (m : HlTlY.carrier), isoF.toLinearMap (isoB.toLinearMap m) = m

theorem adjunction_counit_iso_on_essential_image {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} {rd : PositiveRootData D} (theta : CenterCharacter R g) (Tl : TlambdaData theta) (Hl : HlambdaData theta) (hff : ∀ (Y₁ Y₂ : LieBimodule R g) (hY₁ : IsInHCThetaOne Y₁ theta) (hY₂ : IsInHCThetaOne Y₂ theta), Function.Bijective fun (f : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) => Tl.applyHom f) (hunit : ∀ (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta), have TlY := Tl.applyObj Y hY; let HlTlY := Hl.applyObj TlY; have hHlTlY := ⋯; ∃ (isoF : HCThetaOneHom Y HlTlY theta hY hHlTlY) (isoB : HCThetaOneHom HlTlY Y theta hHlTlY hY), (∀ (m : Y.carrier), isoB.toLinearMap (isoF.toLinearMap m) = m) ∧ ∀ (m : HlTlY.carrier), isoF.toLinearMap (isoB.toLinearMap m) = m) (X : LieModuleObj R g) (hX : IsInO_Lambda rd theta Tl X) : Nonempty (LieModuleIso R g (Tl.applyObj (Hl.applyObj X) ⋯) X)

theorem Tlambda_counit_isomorphism {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [IsNoetherianRing R] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] {D : TriangularDecomposition R g} {rd : PositiveRootData D} (_wg : WeylGroupData D) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd _wg lam) (Tl : TlambdaData theta) (Hl : HlambdaData theta) (X : LieModuleObj R g) : IsInO_Lambda rd theta Tl X → let Y := Hl.applyObj X; have hY := ⋯; Nonempty (LieModuleIso R g (Tl.applyObj Y hY) X)

theorem bernstein_gelfand_25_8_ii {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} [IsNoetherianRing R] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] {rd : PositiveRootData D} (_wg : WeylGroupData D) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd _wg lam) (Tl : TlambdaData theta) (Hl : HlambdaData theta) : (∀ (Y₁ Y₂ : LieBimodule R g) (hY₁ : IsInHCThetaOne Y₁ theta) (hY₂ : IsInHCThetaOne Y₂ theta), Function.Bijective fun (f : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) => Tl.applyHom f) ∧ (∀ (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta), have TlY := Tl.applyObj Y hY; let HlTlY := Hl.applyObj TlY; have hHlTlY := ⋯; ∃ (isoF : HCThetaOneHom Y HlTlY theta hY hHlTlY) (isoB : HCThetaOneHom HlTlY Y theta hHlTlY hY), (∀ (m : Y.carrier), isoB.toLinearMap (isoF.toLinearMap m) = m) ∧ ∀ (m : HlTlY.carrier), isoF.toLinearMap (isoB.toLinearMap m) = m) ∧ ∀ (X : LieModuleObj R g), IsInO_Lambda rd theta Tl X → let Y := Hl.applyObj X; have hY := ⋯; Nonempty (LieModuleIso R g (Tl.applyObj Y hY) X)

theorem theorem_23_6_regular_block_eq {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} {rd : PositiveRootData D} (wg : WeylGroupData D) (cd : RootCorootData rd) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd wg lam) (_hreg : IsRegularWeight wg cd lam) (Tl : TlambdaData theta) (X : LieModuleObj R g) (hBlock : IsInBlock_LambdaPlusP rd X theta) : IsInO_Lambda rd theta Tl X

theorem bernstein_gelfand_25_8_i {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] {D : TriangularDecomposition R g} [IsNoetherianRing R] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] {rd : PositiveRootData D} (wg : WeylGroupData D) (cd : RootCorootData rd) (theta : CenterCharacter R g) (lam : ↥D.𝔥 →ₗ[R] R) (_hdom : IsDominantWeightLE rd wg lam) (_hreg : IsRegularWeight wg cd lam) (Tl : TlambdaData theta) (Hl : HlambdaData theta) : (∀ (Y₁ Y₂ : LieBimodule R g) (hY₁ : IsInHCThetaOne Y₁ theta) (hY₂ : IsInHCThetaOne Y₂ theta), Function.Bijective fun (f : HCThetaOneHom Y₁ Y₂ theta hY₁ hY₂) => Tl.applyHom f) ∧ ∀ (X : LieModuleObj R g), IsInBlock_LambdaPlusP rd X theta → let Y := Hl.applyObj X; have hY := ⋯; Nonempty (LieModuleIso R g (Tl.applyObj Y hY) X)

def IsKFiniteVector {R : Type u_R} [CommRing R] {G : Type u_1} [Group G] {V : Type u_2} [AddCommGroup V] [Module R V] (π : Representation R G V) (K : Subgroup G) (v : V) : Prop

def IsAdmissibleRepresentation {R : Type u_R} [CommRing R] {G : Type u_1} [Group G] {V : Type u_2} [AddCommGroup V] [Module R V] (π : Representation R G V) (K : Subgroup G) : Prop

structure RealizingRepData {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) (M : LieBimodule R g) (_hM : IsInHCThetaOne M theta) : Type (max (max (max (max (u_1 + 1) (u_2 + 1)) u_R) u_g) (u_mod + 1))

• G : Type u_1
• instGroupG : Group self.G
• instTopG : TopologicalSpace self.G
• instTopGroupG : IsTopologicalGroup self.G
• instSCG : SimplyConnectedSpace self.G
• K : Subgroup self.G
• instCompactK : CompactSpace ↥self.K
• V : Type u_2
• instNACGV : NormedAddCommGroup self.V
• instIPSV : InnerProductSpace ℂ self.V
• instCompleteV : CompleteSpace self.V
• instModRV : Module R self.V
• instLieRingModuleGV : LieRingModule g self.V
• instLieModuleGV : LieModule R g self.V
• π : Representation R self.G self.V
• admissible : IsAdmissibleRepresentation self.π self.K
• kFinBimod : LieBimodule R g
• kFinInHCTheta : IsInHCThetaOne self.kFinBimod theta
• embedding : self.kFinBimod.carrier →ₗ[R] self.V
• embedding_injective : Function.Injective ⇑self.embedding
• embedding_lie_compat (x : g) (w : self.kFinBimod.carrier) : self.embedding ((self.kFinBimod.leftAction ((UniversalEnvelopingAlgebra.ι R) x)) w) = ⁅x, self.embedding w⁆
• embedding_KFinite (w : self.kFinBimod.carrier) : IsKFiniteVector self.π self.K (self.embedding w)
• isoForward : HCThetaOneHom self.kFinBimod M theta ⋯ _hM
• isoBackward : HCThetaOneHom M self.kFinBimod theta _hM ⋯
• iso_left_inv (m : M.carrier) : self.isoForward.toLinearMap (self.isoBackward.toLinearMap m) = m
• iso_right_inv (v : self.kFinBimod.carrier) : self.isoBackward.toLinearMap (self.isoForward.toLinearMap v) = v

theorem corollary_6_13_sub_realizable {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] (theta : CenterCharacter R g) (M : LieBimodule R g) (hM : IsInHCThetaOne M theta) (N : LieBimodule R g) (hN : IsInHCThetaOne N theta) (f : HCThetaOneHom M N theta hM hN) (hf_inj : Function.Injective ⇑f.toLinearMap) (h_real : Nonempty (RealizingRepData theta N hN)) : Nonempty (RealizingRepData theta M hM)

theorem tensor_bimodule_has_realizing_data {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] (theta : CenterCharacter R g) (P : LieBimodule R g) (hP : IsInHCThetaOne P theta) (V : Type u_mod) [AddCommGroup V] [Module R V] (hTV : IsTensorProductBimoduleWithUTheta P theta V) : Nonempty (RealizingRepData theta P hP)

theorem hc_theta_one_tensor_bimodule_embeds {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] (theta : CenterCharacter R g) (Y : LieBimodule R g) (hY : IsInHCThetaOne Y theta) : ∃ (I : LieBimodule R g) (hI : IsInHCThetaOne I theta) (W : Type u_mod) (x : AddCommGroup W) (x_1 : Module R W), IsTensorProductBimoduleWithUTheta I theta W ∧ ∃ (ι : HCThetaOneHom Y I theta hY hI), Function.Injective ⇑ι.toLinearMap

noncomputable def embedding_into_realizable_bimodule_core {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] (theta : CenterCharacter R g) (M : LieBimodule R g) (hM : IsInHCThetaOne M theta) : ∃ (N : LieBimodule R g) (hN : IsInHCThetaOne N theta) (f : HCThetaOneHom M N theta hM hN), Function.Injective ⇑f.toLinearMap ∧ Nonempty (RealizingRepData theta N hN)

theorem corollary_25_11_realizability {R : Type u_R} [CommRing R] {g : Type u_g} [LieRing g] [LieAlgebra R g] [LieAlgebra.IsSemisimple R g] [Module.Finite R g] (theta : CenterCharacter R g) (M : LieBimodule R g) (hM : IsInHCThetaOne M theta) : Nonempty (RealizingRepData theta M hM)