structure PS_IsHarishChandraBimodule (R : Type u_1) [CommRing R] (𝔤 : Type u_2) [LieRing 𝔤] [LieAlgebra R 𝔤] (M : Type u_3) [AddCommGroup M] [Module R M] : Type (max u_2 u_3)

• left_action : 𝔤 →ₗ⁅R⁆ Module.End R M
• right_action : 𝔤 →ₗ⁅R⁆ Module.End R M
• actions_comm (x y : 𝔤) (m : M) : (self.left_action x) ((self.right_action y) m) = (self.right_action y) ((self.left_action x) m)
• locally_finite_diag (m : M) : (Submodule.span R (Set.range fun (x : 𝔤) => (self.left_action x) m - (self.right_action x) m)).FG

def IsLocallyFiniteMap (R : Type u_1) [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Type u_4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : Prop

def RestrictedDual (R : Type u_1) [CommRing R] (M : Type u_3) [AddCommGroup M] [Module R M] : Type (max u_1 u_3)

def IsInRestrictedDual (R : Type u_1) [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (f : Module.Dual R M) : Prop

@[reducible, inline]

abbrev liftAct (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (V : Type u_5) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (x : UniversalEnvelopingAlgebra R 𝔤) (v : V) : V

theorem coordinate_ring_faithful (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] [CharZero R] [LieAlgebra.IsSemisimple R 𝔤] : ∃ (OG : Type u_mod) (x : AddCommGroup OG) (x_1 : Module R OG) (x_2 : LieRingModule 𝔤 OG) (x_3 : LieModule R 𝔤 OG), Function.Injective ⇑((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 OG))

theorem coordinate_ring_spanned_by_matrix_coefficients (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] [CharZero R] [LieAlgebra.IsSemisimple R 𝔤] (OG : Type u_mod) [AddCommGroup OG] [Module R OG] [LieRingModule 𝔤 OG] [LieModule R 𝔤 OG] (x : UniversalEnvelopingAlgebra R 𝔤) (m : OG) : ∃ (n : ℕ) (V : Fin n → Type u_mod) (x_1 : (i : Fin n) → AddCommGroup (V i)) (x_2 : (i : Fin n) → Module R (V i)) (x_3 : (i : Fin n) → LieRingModule 𝔤 (V i)) (x_4 : ∀ (i : Fin n), LieModule R 𝔤 (V i)) (_ : ∀ (i : Fin n), LieModule.IsIrreducible R 𝔤 (V i)) (_ : ∀ (i : Fin n), Module.Finite R (V i)) (φ : (i : Fin n) → V i →ₗ[R] OG) (v : (i : Fin n) → V i), liftAct R 𝔤 OG x m = ∑ i : Fin n, (φ i) (liftAct R 𝔤 (V i) x (v i))

theorem coordinate_ring_kill {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [CharZero R] [LieAlgebra.IsSemisimple R 𝔤] (OG : Type u_mod) [AddCommGroup OG] [Module R OG] [LieRingModule 𝔤 OG] [LieModule R 𝔤 OG] (x : UniversalEnvelopingAlgebra R 𝔤) (h_reps : ∀ (V : Type u_mod) [inst : AddCommGroup V] [inst_1 : Module R V] [inst_2 : LieRingModule 𝔤 V] [inst_3 : LieModule R 𝔤 V], LieModule.IsIrreducible R 𝔤 V → Module.Finite R V → ∀ (v : V), liftAct R 𝔤 V x v = 0) (m : OG) : liftAct R 𝔤 OG x m = 0

theorem peter_weyl_faithful_module (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] [CharZero R] [LieAlgebra.IsSemisimple R 𝔤] : ∃ (OG : Type u_mod) (x : AddCommGroup OG) (x_1 : Module R OG) (x_2 : LieRingModule 𝔤 OG) (x_3 : LieModule R 𝔤 OG), (∀ (x_4 : UniversalEnvelopingAlgebra R 𝔤), (∀ (m : OG), (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 OG)) x_4) m = 0) → x_4 = 0) ∧ ∀ (x_4 : UniversalEnvelopingAlgebra R 𝔤), (∀ (V : Type u_mod) [inst : AddCommGroup V] [inst_1 : Module R V] [inst_2 : LieRingModule 𝔤 V] [inst_3 : LieModule R 𝔤 V], LieModule.IsIrreducible R 𝔤 V → Module.Finite R V → ∀ (v : V), (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 V)) x_4) v = 0) → ∀ (m : OG), (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 OG)) x_4) m = 0

theorem residual_finiteness_Ug {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] [CharZero R] [LieAlgebra.IsSemisimple R 𝔤] (x : UniversalEnvelopingAlgebra R 𝔤) (hx : ∀ (V : Type u_mod) [inst : AddCommGroup V] [inst_1 : Module R V] [inst_2 : LieRingModule 𝔤 V] [inst_3 : LieModule R 𝔤 V], LieModule.IsIrreducible R 𝔤 V → Module.Finite R V → ∀ (v : V), (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 V)) x) v = 0) : x = 0

theorem commutator_acts_zero_when_scalar (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] (z x : UniversalEnvelopingAlgebra R 𝔤) (hz : ∀ (V : Type u_mod) [inst : AddCommGroup V] [inst_1 : Module R V] [inst_2 : LieRingModule 𝔤 V] [inst_3 : LieModule R 𝔤 V], LieModule.IsIrreducible R 𝔤 V → Module.Finite R V → ∃ (c : R), ∀ (v : V), (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 V)) z) v = c • v) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] : LieModule.IsIrreducible R 𝔤 V → Module.Finite R V → ∀ (v : V), (((UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R 𝔤 V)) (x * z - z * x)) v = 0

structure PrincipalSeriesBimodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) : Type (max (max u_1 u_2) (u_mod + 1))

• wt_lambda : ↥Δ.𝔥 →ₗ[R] R
• wt_mu : ↥Δ.𝔥 →ₗ[R] R
• M_source : Type u_mod
• M_source_acg : AddCommGroup self.M_source
• M_source_mod : Module R self.M_source
• M_source_lrm : LieRingModule 𝔤 self.M_source
• M_source_lm : LieModule R 𝔤 self.M_source
• verma_source : IsVermaModule Δ self.M_source self.wt_lambda
• M_target : Type u_mod
• M_target_acg : AddCommGroup self.M_target
• M_target_mod : Module R self.M_target
• M_target_lrm : LieRingModule 𝔤 self.M_target
• M_target_lm : LieModule R 𝔤 self.M_target
• verma_target : IsVermaModule Δ self.M_target self.wt_mu

def PrincipalSeriesBimodule.carrierType {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) : Type (max u_1 u_3)

theorem principalSeries_is_HC_bimodule_aux (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) : ∃ (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType), Nonempty (PS_IsHarishChandraBimodule R 𝔤 P.carrierType)

theorem principalSeries_is_HC_bimodule {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) : ∃ (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType), Nonempty (PS_IsHarishChandraBimodule R 𝔤 P.carrierType)

theorem principalSeries_decomposition_aux (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (f : P.carrierType) : ∃ (n : ℕ) (V : Fin n → Type u_mod) (x : (i : Fin n) → AddCommGroup (V i)) (x_1 : (i : Fin n) → Module R (V i)) (x_2 : (i : Fin n) → LieRingModule 𝔤 (V i)) (_ : ∀ (i : Fin n), LieModule R 𝔤 (V i)) (_ : ∀ (i : Fin n), Module.Finite R (V i)) (_ : ∀ (i : Fin n), LieModule.IsIrreducible R 𝔤 (V i)) (φ : (i : Fin n) → (V i →ₗ[R] R) →ₗ[R] P.M_source →ₗ[R] Module.Dual R P.M_target), ↑f ∈ Submodule.span R (⋃ (i : Fin n), Set.range fun (ℓ : V i →ₗ[R] R) => (φ i) ℓ)

structure HCBimoduleHom {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {M : Type u_3} [AddCommGroup M] [Module R M] {N : Type u_4} [AddCommGroup N] [Module R N] (hcM : PS_IsHarishChandraBimodule R 𝔤 M) (hcN : PS_IsHarishChandraBimodule R 𝔤 N) : Type (max u_3 u_4)

• toLinearMap : M →ₗ[R] N
• left_compat (x : 𝔤) (m : M) : self.toLinearMap ((hcM.left_action x) m) = (hcN.left_action x) (self.toLinearMap m)
• right_compat (x : 𝔤) (m : M) : self.toLinearMap ((hcM.right_action x) m) = (hcN.right_action x) (self.toLinearMap m)

def BorelBimoduleHom {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) {X : Type u_3} [AddCommGroup X] [Module R X] (hX : PS_IsHarishChandraBimodule R 𝔤 X) : Type (max u_1 u_3)

def IntermediateBorelHom {R : Type u_3} [CommRing R] {𝔤 : Type u_4} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) {X : Type u_5} [AddCommGroup X] [Module R X] (hX : PS_IsHarishChandraBimodule R 𝔤 X) : Type (max u_3 u_5)

theorem frobenius_induction_adjunction (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (X : Type u_mod) [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : PS_IsHarishChandraBimodule R 𝔤 X) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcM : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) : ∃ (Φ₁ : HCBimoduleHom hX hcM → IntermediateBorelHom P hX), Function.Bijective Φ₁

theorem frobenius_coinduction_adjunction (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (X : Type u_mod) [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : PS_IsHarishChandraBimodule R 𝔤 X) : ∃ (Φ₂ : IntermediateBorelHom P hX → BorelBimoduleHom P hX), Function.Bijective Φ₂

theorem frobenius_reciprocity_principal_series (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (X : Type u_mod) [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : PS_IsHarishChandraBimodule R 𝔤 X) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcM : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) : ∃ (Φ : HCBimoduleHom hX hcM → BorelBimoduleHom P hX), Function.Bijective Φ

theorem principalSeries_representability {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (X : Type u_mod) [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] (hX : PS_IsHarishChandraBimodule R 𝔤 X) (hHC_M : ∃ (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType), Nonempty (PS_IsHarishChandraBimodule R 𝔤 P.carrierType)) : ∃ (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcM : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) (Φ : HCBimoduleHom hX hcM → BorelBimoduleHom P hX), Function.Bijective Φ

structure PS_PositiveRootData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} : Type (max u_1 u_2)

• n_roots : ℕ
• f_root : Fin self.n_roots → 𝔤
• f_root_star : Fin self.n_roots → 𝔤 →ₗ[R] R
• f_root_in_neg (i : Fin self.n_roots) : self.f_root i ∈ Δ.𝔫_neg

def contragredientAction {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {V : Type u_3} [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] (x : 𝔤) (ℓ : V →ₗ[R] R) : V →ₗ[R] R

structure PhiMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] : Type (max (max u_1 u_3) u_mod)

• phi : V → (V →ₗ[R] R) → P.carrierType

def concreteTensorDual {R : Type u_1} [CommRing R] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (f : M →ₗ[R] R) (ℓ : N →ₗ[R] R) : TensorProduct R M N →ₗ[R] R

theorem exercise_8_13_phi_separating (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (Φ : PhiMap P (TensorProduct R 𝔤 V)) (Ψ₁ Ψ₂ : TensorProduct R 𝔤 V →ₗ[R] R) (h_agree : ∀ (v : V) (b : 𝔤), Φ.phi (b ⊗ₜ[R] v) Ψ₁ = Φ.phi (b ⊗ₜ[R] v) Ψ₂) : Ψ₁ = Ψ₂

theorem exercise_8_13_equivariance_and_identification (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcP : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) (roots : PS_PositiveRootData) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (Φ_V : PhiMap P V) (Φ_gV : PhiMap P (TensorProduct R 𝔤 V)) (wt_lambda_ext : 𝔤 →ₗ[R] R) (hwt_compat : ∀ (h : ↥Δ.𝔥), wt_lambda_ext ↑h = P.wt_lambda h) (hwt_npos_zero : ∀ (e : ↥Δ.𝔫_pos), wt_lambda_ext ↑e = 0) (hwt_nneg_zero : ∀ (f : ↥Δ.𝔫_neg), wt_lambda_ext ↑f = 0) (ℓ : V →ₗ[R] R) : ∃ (Ψ : TensorProduct R 𝔤 V →ₗ[R] R), (∀ (v : V) (b : 𝔤), (hcP.right_action b) (Φ_V.phi v ℓ) = Φ_gV.phi (b ⊗ₜ[R] v) Ψ) ∧ Ψ = concreteTensorDual wt_lambda_ext ℓ + ∑ α : Fin roots.n_roots, concreteTensorDual (roots.f_root_star α) (contragredientAction (roots.f_root α) ℓ)

theorem right_action_full_formula {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcP : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) (roots : PS_PositiveRootData) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (Φ_V : PhiMap P V) (Φ_gV : PhiMap P (TensorProduct R 𝔤 V)) (wt_lambda_ext : 𝔤 →ₗ[R] R) (hwt_compat : ∀ (h : ↥Δ.𝔥), wt_lambda_ext ↑h = P.wt_lambda h) (hwt_npos_zero : ∀ (e : ↥Δ.𝔫_pos), wt_lambda_ext ↑e = 0) (hwt_nneg_zero : ∀ (f : ↥Δ.𝔫_neg), wt_lambda_ext ↑f = 0) (v : V) (ℓ : V →ₗ[R] R) (b : 𝔤) : (hcP.right_action b) (Φ_V.phi v ℓ) = Φ_gV.phi (b ⊗ₜ[R] v) (concreteTensorDual wt_lambda_ext ℓ + ∑ α : Fin roots.n_roots, concreteTensorDual (roots.f_root_star α) (contragredientAction (roots.f_root α) ℓ))

theorem principalSeries_right_action {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcP : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) (roots : PS_PositiveRootData) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (Φ_V : PhiMap P V) (Φ_gV : PhiMap P (TensorProduct R 𝔤 V)) (wt_lambda_ext : 𝔤 →ₗ[R] R) (hwt_compat : ∀ (h : ↥Δ.𝔥), wt_lambda_ext ↑h = P.wt_lambda h) (hwt_npos_zero : ∀ (e : ↥Δ.𝔫_pos), wt_lambda_ext ↑e = 0) (hwt_nneg_zero : ∀ (f : ↥Δ.𝔫_neg), wt_lambda_ext ↑f = 0) (v : V) (ℓ : V →ₗ[R] R) (b : 𝔤) : (hcP.right_action b) (Φ_V.phi v ℓ) = Φ_gV.phi (b ⊗ₜ[R] v) (concreteTensorDual wt_lambda_ext ℓ + ∑ α : Fin roots.n_roots, concreteTensorDual (roots.f_root_star α) (contragredientAction (roots.f_root α) ℓ))

structure LieGroupData {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) : Type (max u_2 (u_mod + 1))

• G_c : Type u_mod
• H_c : Type u_mod
• incl : self.H_c → self.G_c
• Ad : self.G_c → 𝔤 →ₗ[R] 𝔤

structure SmoothSectionsFinite {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt_lambda wt_mu : ↥Δ.𝔥 →ₗ[R] R) : Type (max (max u_1 u_2) (u_mod + 1))

• carrier : Type u_mod
• carrier_acg : AddCommGroup self.carrier
• carrier_mod : Module R self.carrier
• hc_structure : PS_IsHarishChandraBimodule R 𝔤 self.carrier
• is_locally_finite (f : self.carrier) : (Submodule.span R (Set.range fun (x : 𝔤) => (self.hc_structure.left_action x) f)).FG
• right_action_cartan_weight (h : ↥Δ.𝔥) (f : self.carrier) : (self.hc_structure.right_action ↑h) f = SMul.smul (wt_mu h) f
• left_action_cartan_weight (h : ↥Δ.𝔥) (f : self.carrier) : (self.hc_structure.left_action ↑h) f = SMul.smul (wt_lambda h) f

structure MatrixCoefficientMap {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (C : SmoothSectionsFinite Δ P.wt_lambda P.wt_mu) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcP : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) : Type (max (max u_1 u_3) u_4)

• toFun : P.carrierType → C.carrier
• map_add (a b : P.carrierType) : self.toFun (a + b) = self.toFun a + self.toFun b
• map_smul (r : R) (a : P.carrierType) : self.toFun (SMul.smul r a) = r • self.toFun a
• injective : Function.Injective self.toFun
• surjective : Function.Surjective self.toFun
• left_compat (x : 𝔤) (f : P.carrierType) : self.toFun ((hcP.left_action x) f) = (C.hc_structure.left_action x) (self.toFun f)
• right_compat (x : 𝔤) (f : P.carrierType) : self.toFun ((hcP.right_action x) f) = (C.hc_structure.right_action x) (self.toFun f)

theorem principalSeries_geometric_realization (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcP : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) : ∃ (C : SmoothSectionsFinite Δ P.wt_lambda P.wt_mu), Nonempty (MatrixCoefficientMap P C inst_acg inst_mod hcP)

structure LieGroupRepresentation {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (G_data : LieGroupData Δ) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] : Type (max u_3 u_mod)

• π : G_data.G_c → V →ₗ[R] V
• π_inv : G_data.G_c → V →ₗ[R] V
• π_inv_left (g : G_data.G_c) (v : V) : (self.π_inv g) ((self.π g) v) = v
• π_inv_right (g : G_data.G_c) (v : V) : (self.π g) ((self.π_inv g) v) = v

structure SmoothSectionsEval {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wt_lambda wt_mu : ↥Δ.𝔥 →ₗ[R] R} (C : SmoothSectionsFinite Δ wt_lambda wt_mu) (G_data : LieGroupData Δ) : Type (max (max u_1 u_3) u_4)

• eval : C.carrier → G_data.G_c → R
• eval_linear (r : R) (f₁ f₂ : C.carrier) (g : G_data.G_c) : self.eval (r • f₁ + f₂) g = r * self.eval f₁ g + self.eval f₂ g
• eval_injective (f₁ f₂ : C.carrier) : (∀ (g : G_data.G_c), self.eval f₁ g = self.eval f₂ g) → f₁ = f₂

theorem prop_19_5_formula (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (P : PrincipalSeriesBimodule Δ) (G_data : LieGroupData Δ) (inst_acg : AddCommGroup P.carrierType) (inst_mod : Module R P.carrierType) (hcP : PS_IsHarishChandraBimodule R 𝔤 P.carrierType) (C : SmoothSectionsFinite Δ P.wt_lambda P.wt_mu) (ξ : MatrixCoefficientMap P C inst_acg inst_mod hcP) (ev : SmoothSectionsEval C G_data) (V : Type u_mod) [AddCommGroup V] [Module R V] [LieRingModule 𝔤 V] [LieModule R 𝔤 V] [Module.Finite R V] (Φ_V : PhiMap P V) (π π_inv : G_data.G_c → V →ₗ[R] V) (hπ_inv : ∀ (g : G_data.G_c) (v : V), (π_inv g) ((π g) v) = v) (hπ_inv' : ∀ (g : G_data.G_c) (v : V), (π g) ((π_inv g) v) = v) (v : V) (ℓ : V →ₗ[R] R) (g : G_data.G_c) : ev.eval (ξ.toFun (Φ_V.phi v ℓ)) g = ℓ ((π_inv g) v)

structure FunctorHLambda {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wt_lambda : ↥Δ.𝔥 →ₗ[R] R) : Type (max (max u_1 u_2) (u_mod + 1))

• M_lambda : Type u_mod
• M_lambda_acg : AddCommGroup self.M_lambda
• M_lambda_mod : Module R self.M_lambda
• M_lambda_lrm : LieRingModule 𝔤 self.M_lambda
• M_lambda_lm : LieModule R 𝔤 self.M_lambda
• verma_lambda : IsVermaModule Δ self.M_lambda wt_lambda

def FunctorHLambda.onObject {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (X : Type u_mod) [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] : Type (max u_mod u_3)

def FunctorHLambda.onMorphism {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) {X Y : Type u_mod} [AddCommGroup X] [Module R X] [LieRingModule 𝔤 X] [LieModule R 𝔤 X] [AddCommGroup Y] [Module R Y] [LieRingModule 𝔤 Y] [LieModule R 𝔤 Y] (φ : X →ₗ⁅R,𝔤⁆ Y) (hx : H.onObject X) : H.onObject Y

theorem functor_H_lambda_on_dual_verma_aux (R : Type u_3) [CommRing R] (𝔤 : Type u_4) [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (wt_mu : ↥Δ.𝔥 →ₗ[R] R) (M_mu : Type u_5) [AddCommGroup M_mu] [Module R M_mu] [LieRingModule 𝔤 M_mu] [LieModule R 𝔤 M_mu] (hM_mu : IsVermaModule Δ M_mu wt_mu) : ∃ (P : PrincipalSeriesBimodule Δ), P.wt_lambda = wt_lambda ∧ P.wt_mu = wt_mu

def IsDominantWeight {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wt : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem prop_16_4_verma_projective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (hdom : IsDominantWeight rd wt_lambda) (X₂ X₃ : Type u_mod) [AddCommGroup X₂] [Module R X₂] [LieRingModule 𝔤 X₂] [LieModule R 𝔤 X₂] [AddCommGroup X₃] [Module R X₃] [LieRingModule 𝔤 X₃] [LieModule R 𝔤 X₃] (hX₂_catO : IsCategoryO Δ rd X₂) (hX₃_catO : IsCategoryO Δ rd X₃) (g : X₂ →ₗ⁅R,𝔤⁆ X₃) (hg_surj : Function.Surjective ⇑g) (h : H.M_lambda →ₗ⁅R,𝔤⁆ X₃) (hlf : IsLocallyFiniteMap R ↑h) : ∃ (lift : H.M_lambda →ₗ⁅R,𝔤⁆ X₂), (∀ (m : H.M_lambda), g (lift m) = h m) ∧ IsLocallyFiniteMap R ↑lift

theorem cor_16_5_tensor_verma_projective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (hdom : IsDominantWeight rd wt_lambda) (X₂ X₃ : Type u_mod) [AddCommGroup X₂] [Module R X₂] [LieRingModule 𝔤 X₂] [LieModule R 𝔤 X₂] [AddCommGroup X₃] [Module R X₃] [LieRingModule 𝔤 X₃] [LieModule R 𝔤 X₃] (hX₂_catO : IsCategoryO Δ rd X₂) (hX₃_catO : IsCategoryO Δ rd X₃) (g : X₂ →ₗ⁅R,𝔤⁆ X₃) (hg_surj : Function.Surjective ⇑g) (h₃ : H.onObject X₃) : ∃ (h₂ : H.onObject X₂), ∀ (m : H.M_lambda), g (↑h₂ m) = ↑h₃ m

theorem functor_H_lambda_injective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (X₁ X₂ : Type u_mod) [AddCommGroup X₁] [Module R X₁] [LieRingModule 𝔤 X₁] [LieModule R 𝔤 X₁] [AddCommGroup X₂] [Module R X₂] [LieRingModule 𝔤 X₂] [LieModule R 𝔤 X₂] (f : X₁ →ₗ⁅R,𝔤⁆ X₂) (hf_inj : Function.Injective ⇑f) (h₁ : H.onObject X₁) (hfh₁ : ∀ (m : H.M_lambda), f (↑h₁ m) = 0) : ↑h₁ = 0

theorem functor_H_lambda_middle_exact {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (X₁ X₂ X₃ : Type u_mod) [AddCommGroup X₁] [Module R X₁] [LieRingModule 𝔤 X₁] [LieModule R 𝔤 X₁] [AddCommGroup X₂] [Module R X₂] [LieRingModule 𝔤 X₂] [LieModule R 𝔤 X₂] [AddCommGroup X₃] [Module R X₃] [LieRingModule 𝔤 X₃] [LieModule R 𝔤 X₃] (f : X₁ →ₗ⁅R,𝔤⁆ X₂) (g : X₂ →ₗ⁅R,𝔤⁆ X₃) (hf_inj : Function.Injective ⇑f) (h_exact : f.range = g.ker) (h₂ : H.onObject X₂) : (∀ (m : H.M_lambda), g (↑h₂ m) = 0) ↔ ∃ (h₁ : H.onObject X₁), ∀ (m : H.M_lambda), f (↑h₁ m) = ↑h₂ m

theorem functor_H_lambda_surjective {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (hdom : IsDominantWeight rd wt_lambda) (X₂ X₃ : Type u_mod) [AddCommGroup X₂] [Module R X₂] [LieRingModule 𝔤 X₂] [LieModule R 𝔤 X₂] [AddCommGroup X₃] [Module R X₃] [LieRingModule 𝔤 X₃] [LieModule R 𝔤 X₃] (hX₂_catO : IsCategoryO Δ rd X₂) (hX₃_catO : IsCategoryO Δ rd X₃) (g : X₂ →ₗ⁅R,𝔤⁆ X₃) (hg_surj : Function.Surjective ⇑g) (h₃ : H.onObject X₃) : ∃ (h₂ : H.onObject X₂), ∀ (m : H.M_lambda), g (↑h₂ m) = ↑h₃ m

theorem functor_H_lambda_exact {R : Type u_1} [CommRing R] {𝔤 : Type u_2} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} {rd : PositiveRootData Δ} {wt_lambda : ↥Δ.𝔥 →ₗ[R] R} (H : FunctorHLambda Δ wt_lambda) (hdom : IsDominantWeight rd wt_lambda) (X₁ X₂ X₃ : Type u_mod) [AddCommGroup X₁] [Module R X₁] [LieRingModule 𝔤 X₁] [LieModule R 𝔤 X₁] [AddCommGroup X₂] [Module R X₂] [LieRingModule 𝔤 X₂] [LieModule R 𝔤 X₂] [AddCommGroup X₃] [Module R X₃] [LieRingModule 𝔤 X₃] [LieModule R 𝔤 X₃] (hX₂_catO : IsCategoryO Δ rd X₂) (hX₃_catO : IsCategoryO Δ rd X₃) (f : X₁ →ₗ⁅R,𝔤⁆ X₂) (g : X₂ →ₗ⁅R,𝔤⁆ X₃) (hf_inj : Function.Injective ⇑f) (hg_surj : Function.Surjective ⇑g) (h_exact : f.range = g.ker) : (∀ (h₁ : H.onObject X₁), (∀ (m : H.M_lambda), f (↑h₁ m) = 0) → ↑h₁ = 0) ∧ (∀ (h₂ : H.onObject X₂), (∀ (m : H.M_lambda), g (↑h₂ m) = 0) ↔ ∃ (h₁ : H.onObject X₁), ∀ (m : H.M_lambda), f (↑h₁ m) = ↑h₂ m) ∧ ∀ (h₃ : H.onObject X₃), ∃ (h₂ : H.onObject X₂), ∀ (m : H.M_lambda), g (↑h₂ m) = ↑h₃ m