English
The same as a previous Gallois connection: map and comap form a Galois connection.
Русский
Та же Галуа связь: отображение и обратный образ образуют связь Галуа.
LaTeX
$$GaloisConnection (map f) (comap f)$$
Lean4
theorem isIdealMorphism_iff : f.IsIdealMorphism ↔ ∀ (x : L') (y : L), ∃ z : L, ⁅x, f y⁆ = f z :=
by
simp only [isIdealMorphism_def, idealRange_eq_lieSpan_range, ← LieSubalgebra.toSubmodule_inj,
← f.range.coe_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff,
LieSubalgebra.mem_toSubmodule, mem_range, exists_imp, Submodule.exists_lieSubmodule_coe_eq_iff]
constructor
· intro h x y; obtain ⟨z, hz⟩ := h x (f y) y rfl; use z; exact hz.symm
· intro h x y z hz; obtain ⟨w, hw⟩ := h x z; use w; rw [← hw, hz]
