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
h : Function.Surjective ↑f
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, 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
h : Function.Surjective ↑f
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆
suffices ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆ by exact le_antisymm (map_bracket_le f) this
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
h : Function.Surjective ↑f
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ≤ Submodule.span R (↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m})
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
h : Function.Surjective ↑f
⊢ ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
rw [← LieSubmodule.coeSubmodule_le_coeSubmodule, coe_map_of_surjective h,
  LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
  LinearMap.map_span]
case h
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
h : Function.Surjective ↑f
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
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
h : Function.Surjective ↑f
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ≤ Submodule.span R (↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m})
apply Submodule.span_mono
case h.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
h : Function.Surjective ↑f
z₁ : L'
h₁ : z₁ ∈ map f I₁
z₂ : L'
h₂ : z₂ ∈ map f I₂
⊢ ⁅↑{ val := z₁, property := h₁ }, ↑{ val := z₂, property := h₂ }⁆ ∈ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case h
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
h : Function.Surjective ↑f
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
rintro x ⟨⟨z₁, h₁⟩, ⟨z₂, h₂⟩, rfl⟩
case h.intro.mk.intro.mk.intro
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
h : Function.Surjective ↑f
z₂ : L'
h₂ : z₂ ∈ map f I₂
y₁ : { x // x ∈ I₁ }
h₁ : ↑f ↑y₁ ∈ map f I₁
⊢ ⁅↑{ val := ↑f ↑y₁, property := h₁ }, ↑{ val := z₂, property := h₂ }⁆ ∈ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case h.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
h : Function.Surjective ↑f
z₁ : L'
h₁ : z₁ ∈ map f I₁
z₂ : L'
h₂ : z₂ ∈ map f I₂
⊢ ⁅↑{ val := z₁, property := h₁ }, ↑{ val := z₂, property := h₂ }⁆ ∈ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁
case h.intro.mk.intro.mk.intro.intro
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
h : Function.Surjective ↑f
y₁ : { x // x ∈ I₁ }
h₁ : ↑f ↑y₁ ∈ map f I₁
y₂ : { x // x ∈ I₂ }
h₂ : ↑f ↑y₂ ∈ map f I₂
⊢ ⁅↑{ val := ↑f ↑y₁, property := h₁ }, ↑{ val := ↑f ↑y₂, property := h₂ }⁆ ∈ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
case h.intro.mk.intro.mk.intro
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
h : Function.Surjective ↑f
z₂ : L'
h₂ : z₂ ∈ map f I₂
y₁ : { x // x ∈ I₁ }
h₁ : ↑f ↑y₁ ∈ map f I₁
⊢ ⁅↑{ val := ↑f ↑y₁, property := h₁ }, ↑{ val := z₂, property := h₂ }⁆ ∈ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
obtain ⟨y₂, rfl⟩ := mem_map_of_surjective h h₂
no goals
case h.intro.mk.intro.mk.intro.intro
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
h : Function.Surjective ↑f
y₁ : { x // x ∈ I₁ }
h₁ : ↑f ↑y₁ ∈ map f I₁
y₂ : { x // x ∈ I₂ }
h₂ : ↑f ↑y₂ ∈ map f I₂
⊢ ⁅↑{ val := ↑f ↑y₁, property := h₁ }, ↑{ val := ↑f ↑y₂, property := h₂ }⁆ ∈ ↑↑f '' {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
exact ⟨⁅(y₁ : L), (y₂ : L)⁆, ⟨y₁, y₂, rfl⟩, by apply f.map_lie⟩
no goals
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
h : Function.Surjective ↑f
this : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆
⊢ map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆
exact le_antisymm (map_bracket_le f) this
no goals
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
h : Function.Surjective ↑f
y₁ : { x // x ∈ I₁ }
h₁ : ↑f ↑y₁ ∈ map f I₁
y₂ : { x // x ∈ I₂ }
h₂ : ↑f ↑y₂ ∈ map f I₂
⊢ ↑↑f ⁅↑y₁, ↑y₂⁆ = ⁅↑{ val := ↑f ↑y₁, property := h₁ }, ↑{ val := ↑f ↑y₂, property := h₂ }⁆
apply f.map_lie