theorem
textbook_axiom_internalHom_isCategoryO
{R : Type u}
[CommRing R]
{𝔤 : Type u}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{V : Type u}
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
[Module.Finite R V]
(X : Type u)
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
:
IsCategoryO Δ rd (V →ₗ[R] X)
theorem
postcomp_surjective_of_free
{R : Type u}
[CommRing R]
{V : Type u}
[AddCommGroup V]
[Module R V]
[Module.Free R V]
{X : Type u}
[AddCommGroup X]
[Module R X]
{Y : Type u}
[AddCommGroup Y]
[Module R Y]
(f : X →ₗ[R] Y)
(hf : Function.Surjective ⇑f)
:
Function.Surjective fun (φ : V →ₗ[R] X) => f ∘ₗ φ
theorem
textbook_axiom_internalHom_categoryO_data
{R : Type u}
[CommRing R]
{𝔤 : Type u}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{V : Type u}
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
[Module.Finite R V]
[Module.Free R V]
(X : Type u)
[AddCommGroup X]
[Module R X]
[LieRingModule 𝔤 X]
[LieModule R 𝔤 X]
(hXO : IsCategoryO Δ rd X)
:
IsCategoryO Δ rd (V →ₗ[R] X) ∧ ∀ (Y : Type u) [inst : AddCommGroup Y] [inst_1 : Module R Y] [inst_2 : LieRingModule 𝔤 Y] [LieModule R 𝔤 Y]
(f : X →ₗ⁅R,𝔤⁆ Y), Function.Surjective ⇑f → Function.Surjective fun (φ : V →ₗ[R] X) => ↑f ∘ₗ φ
def
lieModuleHomPostcomp
{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]
{M : Type u_4}
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
{N : Type u_5}
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(f : M →ₗ⁅R,𝔤⁆ N)
:
Instances For
def
lieModuleHomFlip
{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]
{P : Type u_4}
[AddCommGroup P]
[Module R P]
[LieRingModule 𝔤 P]
[LieModule R 𝔤 P]
{N : Type u_5}
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(ψ : V →ₗ⁅R,𝔤⁆ P →ₗ[R] N)
:
Instances For
theorem
textbook_axiom_tensorHom_adjunction_data
{R : Type u}
[CommRing R]
{𝔤 : Type u}
[LieRing 𝔤]
[LieAlgebra R 𝔤]
{Δ : TriangularDecomposition R 𝔤}
{rd : PositiveRootData Δ}
{P : Type u}
[AddCommGroup P]
[Module R P]
[LieRingModule 𝔤 P]
[LieModule R 𝔤 P]
{V : Type u}
[AddCommGroup V]
[Module R V]
[LieRingModule 𝔤 V]
[LieModule R 𝔤 V]
[Module.Finite R V]
[Module.Free R V]
(M : Type u)
[AddCommGroup M]
[Module R M]
[LieRingModule 𝔤 M]
[LieModule R 𝔤 M]
(hMO : IsCategoryO Δ rd M)
(N : Type u)
[AddCommGroup N]
[Module R N]
[LieRingModule 𝔤 N]
[LieModule R 𝔤 N]
(hNO : IsCategoryO Δ rd N)
(f : M →ₗ⁅R,𝔤⁆ N)
(hf : Function.Surjective ⇑f)
(g : TensorProduct R V P →ₗ⁅R,𝔤⁆ N)
:
∃ (W_M : Type u) (x : AddCommGroup W_M) (x_1 : Module R W_M) (x_2 : LieRingModule 𝔤 W_M) (x_3 : LieModule R 𝔤 W_M) (_ :
IsCategoryO Δ rd W_M) (W_N : Type u) (x_4 : AddCommGroup W_N) (x_5 : Module R W_N) (x_6 : LieRingModule 𝔤 W_N) (x_7 :
LieModule R 𝔤 W_N) (_ : IsCategoryO Δ rd W_N) (W_f : W_M →ₗ⁅R,𝔤⁆ W_N) (_ : Function.Surjective ⇑W_f) (g' :
P →ₗ⁅R,𝔤⁆ W_N),
∀ (h' : P →ₗ⁅R,𝔤⁆ W_M),
(∀ (p : P), W_f (h' p) = g' p) → ∃ (h : TensorProduct R V P →ₗ⁅R,𝔤⁆ M), ∀ (x : TensorProduct R V P), f (h x) = g x