Ado.ForMathlib.LieModuleHom

@[instance_reducible]

instance LieModuleHom.instMul_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Mul (M →ₗ⁅R,L⁆ M)

Equations

LieModuleHom.instMul_ado = { mul := fun (f g : M →ₗ⁅R,L⁆ M) => f.comp g }

source

theorem LieModuleHom.mul_eq_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (f g : M →ₗ⁅R,L⁆ M) :

f * g = f.comp g

source

@[simp]

theorem LieModuleHom.mul_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] (f g : M →ₗ⁅R,L⁆ M) (x : M) :

(f * g) x = f (g x)

source

@[simp]

theorem LieModuleHom.toLinearMap_one (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

↑1 = 1

source

theorem LieModuleHom.one_eq_id {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

1 = id

source

theorem LieModuleHom.range_id {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

id.range = ⊤

source

theorem LieModuleHom.range_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [LieRingModule L M] [LieRingModule L M₂] [LieRingModule L M₃] (f : M₂ →ₗ⁅R,L⁆ M₃) (g : M →ₗ⁅R,L⁆ M₂) :

(f.comp g).range = LieSubmodule.map f g.range

source

@[simp]

theorem LieModuleHom.range_eq_bot {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (f : M →ₗ⁅R,L⁆ M₂) :

f.range = ⊥ ↔ f = 0

source

theorem LieModuleHom.ker_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [LieRingModule L M] [LieRingModule L M₂] [LieRingModule L M₃] (f : M →ₗ⁅R,L⁆ M₂) (g : M₂ →ₗ⁅R,L⁆ M₃) :

(g.comp f).ker = LieSubmodule.comap f g.ker

source

@[simp]

theorem LieModuleHom.ker_eq_top {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (f : M →ₗ⁅R,L⁆ M₂) :

f.ker = ⊤ ↔ f = 0

source

@[simp]

theorem LieModuleHom.toLinearMap_mul {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (f g : M →ₗ⁅R,L⁆ M) :

↑(f * g) = ↑f * ↑g

source

@[instance_reducible]

instance LieModuleHom.instMonoid_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Monoid (M →ₗ⁅R,L⁆ M)

Equations

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

source

@[simp]

theorem LieModuleHom.toLinearMap_zero (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

↑0 = 0

source

instance LieModuleHom.instIsMulApplyEqComp_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

IsMulApplyEqComp (M →ₗ⁅R,L⁆ M) M

source

@[simp]

theorem LieModuleHom.toLinearMap_pow {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (f : M →ₗ⁅R,L⁆ M) (n : ℕ) :

↑(f ^ n) = ↑f ^ n

source

def LieModuleHom.restrict {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (f : M →ₗ⁅R,L⁆ M₂) {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M₂} (h : ∀ x ∈ N, f x ∈ N₂) :

↥N →ₗ⁅R,L⁆ ↥N₂

Equations

f.restrict h = { toLinearMap := (↑f).restrict h, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieModuleHom.restrict_toLinearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (f : M →ₗ⁅R,L⁆ M₂) {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M₂} (h : ∀ x ∈ N, f x ∈ N₂) :

↑(f.restrict h) = (↑f).restrict h

source

@[simp]

theorem LieModuleHom.coe_restrict {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (f : M →ₗ⁅R,L⁆ M₂) {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M₂} (h : ∀ x ∈ N, f x ∈ N₂) :

⇑(f.restrict h) = Set.MapsTo.restrict (⇑f) (↑N) (↑N₂) h

source

@[simp]

theorem LieModuleHom.isNilpotent_toLinearMap {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (f : M →ₗ⁅R,L⁆ M) :

IsNilpotent ↑f ↔ IsNilpotent f

source

theorem LieSubmodule.comap_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [LieRingModule L M] [LieRingModule L M₂] [LieRingModule L M₃] (f : M →ₗ⁅R,L⁆ M₂) (g : M₂ →ₗ⁅R,L⁆ M₃) (N : LieSubmodule R L M₃) :

comap (g.comp f) N = comap f (comap g N)

source

@[simp]

theorem LieSubmodule.mem_map_equiv {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] {e : M ≃ₗ⁅R,L⁆ M₂} {N : LieSubmodule R L M} {x : M₂} :

x ∈ map e.toLieModuleHom N ↔ e.symm x ∈ N

source

theorem LieSubmodule.map_equiv_eq_comap_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) (N : LieSubmodule R L M) :

map e.toLieModuleHom N = comap e.symm.toLieModuleHom N

source

theorem LieSubmodule.comap_equiv_eq_map_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) (N : LieSubmodule R L M₂) :

comap e.toLieModuleHom N = map e.symm.toLieModuleHom N

source

theorem LieModuleEquiv.toLieModuleHom_trans {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_5} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M] [Module R M₂] [Module R M₃] [LieRingModule L M] [LieRingModule L M₂] [LieRingModule L M₃] (e : M ≃ₗ⁅R,L⁆ M₂) (e₂ : M₂ ≃ₗ⁅R,L⁆ M₃) :

(e.trans e₂).toLieModuleHom = e₂.comp e.toLieModuleHom

source

@[simp]

theorem LieModuleEquiv.toLieModuleHom_refl {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

refl.toLieModuleHom = LieModuleHom.id

source

@[simp]

theorem LieModuleEquiv.comp_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) :

e.comp e.symm.toLieModuleHom = LieModuleHom.id

source

@[simp]

theorem LieModuleEquiv.symm_comp {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] (e : M ≃ₗ⁅R,L⁆ M₂) :

e.symm.comp e.toLieModuleHom = LieModuleHom.id