Ado.ForMathlib.LieHom

@[simp]

theorem LieHom.coe_mk' {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ[R] L₂) (h : ∀ {x y : L}, f.toFun ⁅x, y⁆ = ⁅f.toFun x, f.toFun y⁆) :

⇑{ toLinearMap := f, map_lie' := h } = ⇑f

{name}coe_mk の一般化

source

def LieHom.lieIdealComap {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) :

↥(LieIdeal.comap f q) →ₗ⁅R⁆ ↥q

Equations

f.lieIdealComap q = { toLinearMap := (↑f).submoduleComap (↑R L₂ q).toSubmodule, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieHom.lieIdealComap_apply_coe {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) (x : ↥(LieIdeal.comap f q)) :

↑((f.lieIdealComap q) x) = f ↑x

source

@[simp]

theorem LieHom.lieIdealComap_surjective_of_surjective {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) (hf : Function.Surjective ⇑f) :

Function.Surjective ⇑(f.lieIdealComap q)

source

@[simp]

theorem LieHom.lieIdealComap_ker {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) :

(f.lieIdealComap q).ker = f.ker.lieIdealOf (LieIdeal.comap f q)

source

def LieHom.lieIdealMap {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (I : LieIdeal R L) :

↥I →ₗ⁅R⁆ ↥(LieIdeal.map f I)

Equations

f.lieIdealMap I = { toLinearMap := Submodule.inclusion ⋯ ∘ₗ (↑f).submoduleMap (↑R L I).toSubmodule, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieHom.lieIdealMap_toLinearMap {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (I : LieIdeal R L) :

↑(f.lieIdealMap I) = Submodule.inclusion ⋯ ∘ₗ (↑f).submoduleMap (↑R L I).toSubmodule

source

@[simp]

theorem LieHom.lieIdealMap_apply_coe {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (I : LieIdeal R L) (x : ↥I) :

↑((f.lieIdealMap I) x) = f ↑x

source

@[simp]

theorem LieHom.lieIdealMap_injective_of_injective {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (I : LieIdeal R L) (hf : Function.Injective ⇑f) :

Function.Injective ⇑(f.lieIdealMap I)

source

@[simp]

theorem LieHom.lieIdealMap_surjective_of_image_eq_map {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (I : LieIdeal R L) (hI : ⇑f '' ↑I = ↑(LieIdeal.map f I)) :

Function.Surjective ⇑(f.lieIdealMap I)

source

@[simp]

theorem LieHom.lieIdealMap_ker {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (I : LieIdeal R L) :

(f.lieIdealMap I).ker = f.ker.lieIdealOf I

source

def LieHom.toSpanSingleton (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :

R →ₗ⁅R⁆ L

Equations

LieHom.toSpanSingleton R L x = { toLinearMap := LinearMap.toSpanSingleton R L x, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieHom.toSpanSingleton_toLinearMap (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) :

↑(toSpanSingleton R L x) = LinearMap.toSpanSingleton R L x

source

@[simp]

theorem LieHom.toSpanSingleton_apply (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (b : R) :

(toSpanSingleton R L x) b = b • x

source

theorem LieHom.ker_comp {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} {L₃ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L →ₗ⁅R⁆ L₂) (g : L₂ →ₗ⁅R⁆ L₃) :

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

source

@[simp]

theorem LieEquiv.toLieHom_refl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] :

refl.toLieHom = LieHom.id

source

@[simp]

theorem LieEquiv.coe_mk {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (g : L₂ → L) (h : Function.LeftInverse g (↑f).toFun) (h₂ : Function.RightInverse g (↑f).toFun) :

⇑{ toLieHom := f, invFun := g, left_inv := h, right_inv := h₂ } = ⇑f

source

@[simp]

theorem LieEquiv.coe_symm_mk {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (g : L₂ → L) (h : Function.LeftInverse g (↑f).toFun) (h₂ : Function.RightInverse g (↑f).toFun) :

⇑{ toLieHom := f, invFun := g, left_inv := h, right_inv := h₂ }.symm = g

source

@[simp]

theorem LieEquiv.comp_symm {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) :

e.comp e.symm.toLieHom = LieHom.id

source

@[simp]

theorem LieEquiv.symm_comp {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) :

e.symm.comp e.toLieHom = LieHom.id

source

theorem LieEquiv.map_equiv_eq_comap_symm {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) (I : LieIdeal R L) :

LieIdeal.map e.toLieHom I = LieIdeal.comap e.symm.toLieHom I

source

theorem LieEquiv.comap_equiv_eq_map_symm {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) (I : LieIdeal R L₂) :

LieIdeal.comap e.toLieHom I = LieIdeal.map e.symm.toLieHom I

source

@[simp]

theorem LieEquiv.mem_map_equiv {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] {e : L ≃ₗ⁅R⁆ L₂} {I : LieIdeal R L} {x : L₂} :

x ∈ LieIdeal.map e.toLieHom I ↔ e.symm x ∈ I

source

@[simp]

theorem LieEquiv.coe_map_equiv {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) (I : LieIdeal R L) :

↑(LieIdeal.map e.toLieHom I) = ⇑e '' ↑I

source

@[simp]

theorem LieEquiv.ker_eq {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) :

e.ker = ⊥

source

def LieEquiv.lieIdealMap {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) (I : LieIdeal R L) :

↥I ≃ₗ⁅R⁆ ↥(LieIdeal.map e.toLieHom I)

Equations

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

Instances For

source

@[simp]

theorem LieEquiv.lieIdealMap_apply_coe {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) (I : LieIdeal R L) (x : ↥I) :

↑((e.lieIdealMap I) x) = e ↑x

source

theorem LieIdeal.surjective_map_of_surjective {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (hf : Function.Surjective ⇑f) :

Function.Surjective (map f)

source

theorem LieIdeal.comap_comp {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} {L₃ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L →ₗ⁅R⁆ L₂) (g : L₂ →ₗ⁅R⁆ L₃) (I : LieIdeal R L₃) :

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

source

theorem LieIdeal.map_comp {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} {L₃ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L →ₗ⁅R⁆ L₂) (g : L₂ →ₗ⁅R⁆ L₃) (I : LieIdeal R L) :

map (g.comp f) I = map g (map f I)

source

@[simp]

theorem LieIdeal.comap_id {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

comap LieHom.id I = I

source

@[simp]

theorem LieIdeal.map_id {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

map LieHom.id I = I

source

@[simp]

theorem LieIdeal.comap_bot {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) :

comap f ⊥ = f.ker