R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
⊢ ⁅I₁, I₂⁆ ≤ comap f ⁅map f I₁, map f I₂⁆
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
⊢ map f ⁅I₁, I₂⁆ ≤ ⁅map f I₁, map f I₂⁆
rw [map_le_iff_le_comap]
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑(comap f ⁅map f I₁, map f I₂⁆)
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
⊢ ⁅I₁, I₂⁆ ≤ comap f ⁅map f I₁, map f I₂⁆
erw [LieSubmodule.lieSpan_le]
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x : L
hx : x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ x ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑(comap f ⁅map f I₁, map f I₂⁆)
intro x hx
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
⊢ x ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x : L
hx : x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
⊢ x ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
obtain ⟨⟨y₁, hy₁⟩, ⟨y₂, hy₂⟩, hx⟩ := hx
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
⊢ x ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
rw [← hx]
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
let fy₁ : ↥(map f I₁) := ⟨f y₁, mem_map hy₁⟩
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
fy₂ : { x // x ∈ map f I₂ } := { val := ↑f y₂, property := (_ : ↑f y₂ ∈ map f I₂) }
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
let fy₂ : ↥(map f I₂) := ⟨f y₂, mem_map hy₂⟩
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
fy₂ : { x // x ∈ map f I₂ } := { val := ↑f y₂, property := (_ : ↑f y₂ ∈ map f I₂) }
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ comap f ⁅map f I₁, map f I₂⁆
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
fy₂ : { x // x ∈ map f I₂ } := { val := ↑f y₂, property := (_ : ↑f y₂ ∈ map f I₂) }
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ ↑(comap f ⁅map f I₁, map f I₂⁆)
change _ ∈ comap f ⁅map f I₁, map f I₂⁆
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
fy₂ : { x // x ∈ map f I₂ } := { val := ↑f y₂, property := (_ : ↑f y₂ ∈ map f I₂) }
⊢ ⁅↑f y₁, ↑f y₂⁆ ∈ ⁅map f I₁, map f I₂⁆
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
fy₂ : { x // x ∈ map f I₂ } := { val := ↑f y₂, property := (_ : ↑f y₂ ∈ map f I₂) }
⊢ ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ ∈ comap f ⁅map f I₁, map f I₂⁆
simp only [Submodule.coe_mk, mem_comap, LieHom.map_lie]
no goals
case intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J : LieIdeal R L'
I₁ I₂ : LieIdeal R L
x y₁ : L
hy₁ : y₁ ∈ I₁
y₂ : L
hy₂ : y₂ ∈ I₂
hx : ⁅↑{ val := y₁, property := hy₁ }, ↑{ val := y₂, property := hy₂ }⁆ = x
fy₁ : { x // x ∈ map f I₁ } := { val := ↑f y₁, property := (_ : ↑f y₁ ∈ map f I₁) }
fy₂ : { x // x ∈ map f I₂ } := { val := ↑f y₂, property := (_ : ↑f y₂ ∈ map f I₂) }
⊢ ⁅↑f y₁, ↑f y₂⁆ ∈ ⁅map f I₁, map f I₂⁆
exact LieSubmodule.lie_coe_mem_lie _ _ fy₁ fy₂