def LieSubmodule.equivSubmoduleOfTrivial (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule.IsTrivial L M] : LieSubmodule R L M ≃o Submodule R M

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieSubmodule.equivSubmoduleOfTrivial_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule.IsTrivial L M] (N : LieSubmodule R L M) : (equivSubmoduleOfTrivial R L M) N = ↑N

@[simp]

theorem LieSubmodule.toSubmodule_equivSubmoduleOfTrivial_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule.IsTrivial L M] (N : Submodule R M) : ↑((equivSubmoduleOfTrivial R L M).symm N) = N

@[simp]

theorem LieSubmodule.mem_equivSubmoduleOfTrivial_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule.IsTrivial L M] (x : M) (N : Submodule R M) : x ∈ (equivSubmoduleOfTrivial R L M).symm N ↔ x ∈ N

instance TrivialLieModule.instFinite_ado {R : Type u_4} {L : Type u_5} {M : Type u_6} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Module.Finite R (TrivialLieModule R L M)

theorem LieModuleHom.injective_or_eq_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule.IsIrreducible R L M] (f : M →ₗ⁅R,L⁆ M₂) : Function.Injective ⇑f ∨ f = 0

theorem LieModuleHom.injective_of_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule.IsIrreducible R L M] {f : M →ₗ⁅R,L⁆ M₂} (h : f ≠ 0) : Function.Injective ⇑f

theorem LieModuleHom.surjective_or_eq_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule.IsIrreducible R L M₂] (f : M →ₗ⁅R,L⁆ M₂) : Function.Surjective ⇑f ∨ f = 0

theorem LieModuleHom.surjective_of_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule.IsIrreducible R L M₂] {f : M →ₗ⁅R,L⁆ M₂} (h : f ≠ 0) : Function.Surjective ⇑f

theorem LieModuleHom.bijective_of_ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule.IsIrreducible R L M] [LieModule.IsIrreducible R L M₂] {f : M →ₗ⁅R,L⁆ M₂} (h : f ≠ 0) : Function.Bijective ⇑f

theorem LieModuleHom.bijective_or_eq_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule.IsIrreducible R L M] [LieModule.IsIrreducible R L M₂] (f : M →ₗ⁅R,L⁆ M₂) : Function.Bijective ⇑f ∨ f = 0

theorem Field.nonempty_lieModuleEquiv_of_isIrreducible_of_isTrivial (K : Type u_5) (L : Type u_6) (V : Type u_7) [Field K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [LieModule.IsIrreducible K L V] [LieModule.IsTrivial L V] : Nonempty (V ≃ₗ⁅K,L⁆ TrivialLieModule K L K)