Documentation

Ado.ForMathlib.LieModuleProd

@[instance_reducible]

instance Prod.instLieRingModule_ado {L : Type u_2} {M : Type u_3} {N : Type u_4} [LieRing L] [AddCommGroup M] [AddCommGroup N] [LieRingModule L M] [LieRingModule L N] :

LieRingModule L (M × N)

Equations

Prod.instLieRingModule_ado = { bracket := fun (x : L) (p : M × N) => (⁅x, p.1⁆, ⁅x, p.2⁆), add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

theorem Prod.lie_module_bracket_def {L : Type u_2} {M : Type u_3} {N : Type u_4} [LieRing L] [AddCommGroup M] [AddCommGroup N] [LieRingModule L M] [LieRingModule L N] (x : L) (p : M × N) :

⁅x, p⁆ = (⁅x, p.1⁆, ⁅x, p.2⁆)

@[simp]

theorem Prod.fst_lie_module_bracket {L : Type u_2} {M : Type u_3} {N : Type u_4} [LieRing L] [AddCommGroup M] [AddCommGroup N] [LieRingModule L M] [LieRingModule L N] (x : L) (p : M × N) :

⁅x, p⁆.1 = ⁅x, p.1⁆

@[simp]

theorem Prod.snd_lie_module_bracket {L : Type u_2} {M : Type u_3} {N : Type u_4} [LieRing L] [AddCommGroup M] [AddCommGroup N] [LieRingModule L M] [LieRingModule L N] (x : L) (p : M × N) :

⁅x, p⁆.2 = ⁅x, p.2⁆

@[simp]

theorem Prod.lie_module_bracket_mk {L : Type u_2} {M : Type u_3} {N : Type u_4} [LieRing L] [AddCommGroup M] [AddCommGroup N] [LieRingModule L M] [LieRingModule L N] (x : L) (m : M) (n : N) :

⁅x, (m, n)⁆ = (⁅x, m⁆, ⁅x, n⁆)

instance Prod.instLieModule_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L M] [LieModule R L N] :

LieModule R L (M × N)

def LieModuleHom.inl (R : Type u_1) (L : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

M →ₗ⁅R,L⁆ M × N

Equations

LieModuleHom.inl R L M N = { toLinearMap := LinearMap.inl R M N, map_lie' := ⋯ }

Instances For

@[simp]

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

(inl R L M N) i = (i, 0)

@[simp]

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

↑(inl R L M N) = LinearMap.inl R M N

def LieModuleHom.inr (R : Type u_1) (L : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

N →ₗ⁅R,L⁆ M × N

Equations

LieModuleHom.inr R L M N = { toLinearMap := LinearMap.inr R M N, map_lie' := ⋯ }

Instances For

@[simp]

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

↑(inr R L M N) = LinearMap.inr R M N

@[simp]

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

(inr R L M N) i = (0, i)

def LieSubmodule.prod {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (p : LieSubmodule R L M) (q : LieSubmodule R L N) :

LieSubmodule R L (M × N)

Equations

p.prod q = { toSubmodule := (↑p).prod ↑q, lie_mem := ⋯ }

Instances For

@[simp]

theorem LieSubmodule.prod_toSubmodule {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (p : LieSubmodule R L M) (q : LieSubmodule R L N) :

↑(p.prod q) = (↑p).prod ↑q

@[simp]

theorem LieSubmodule.coe_prod {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (p : LieSubmodule R L M) (q : LieSubmodule R L N) :

↑(p.prod q) = ↑p ×ˢ ↑q

@[simp]

theorem LieSubmodule.mem_prod {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (p : LieSubmodule R L M) (q : LieSubmodule R L N) (x : M × N) :

x ∈ p.prod q ↔ x.1 ∈ p ∧ x.2 ∈ q

theorem LieSubmodule.prod_eq_sup_map {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (p : LieSubmodule R L M) (q : LieSubmodule R L N) :

p.prod q = map (LieModuleHom.inl R L M N) p ⊔ map (LieModuleHom.inr R L M N) q

@[simp]

theorem LieSubmodule.prod_top {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

⊤.prod ⊤ = ⊤

@[simp]

theorem LieSubmodule.prod_bot {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

⊥.prod ⊥ = ⊥

theorem LieSubmodule.prod_eq_top_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (p : LieSubmodule R L M) (q : LieSubmodule R L N) :

p.prod q = ⊤ ↔ p = ⊤ ∧ q = ⊤

theorem LieSubmodule.prod_eq_bot_iff {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (p : LieSubmodule R L M) (q : LieSubmodule R L N) :

p.prod q = ⊥ ↔ p = ⊥ ∧ q = ⊥

@[simp]

theorem LieSubmodule.lie_module_bracket_prod {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L M] [LieModule R L N] (I : LieIdeal R L) (P : LieSubmodule R L M) (Q : LieSubmodule R L N) :

⁅I, P.prod Q⁆ = ⁅I, P⁆.prod ⁅I, Q⁆

@[simp]

theorem LieSubmodule.lcs_prod {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L M] [LieModule R L N] (P : LieSubmodule R L M) (Q : LieSubmodule R L N) (n : ℕ) :

lcs n (P.prod Q) = (lcs n P).prod (lcs n Q)

@[simp]

theorem Prod.lowerCentralSeries_eq {R : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L M] [LieModule R L N] (n : ℕ) :

LieModule.lowerCentralSeries R L (M × N) n = (LieModule.lowerCentralSeries R L M n).prod (LieModule.lowerCentralSeries R L N n)

@[simp]

theorem Prod.isNilpotent_iff {L : Type u_2} {M : Type u_3} {N : Type u_4} [LieRing L] [AddCommGroup M] [AddCommGroup N] [LieRingModule L M] [LieRingModule L N] :

LieModule.IsNilpotent L (M × N) ↔ LieModule.IsNilpotent L M ∧ LieModule.IsNilpotent L N

instance Prod.instIsNilpotent_ado {L : Type u_2} {M : Type u_3} {N : Type u_4} [LieRing L] [AddCommGroup M] [AddCommGroup N] [LieRingModule L M] [LieRingModule L N] [LieModule.IsNilpotent L M] [LieModule.IsNilpotent L N] :

LieModule.IsNilpotent L (M × N)