instIsTwoSidedMapRingHomOfRingHomSurjective

English

For a surjective ring hom f, the ideal map equals the Submodule map: I.map f = Submodule.map f.toSemilinearMap I.

Русский

Для сюръективного кольмоха f: I.map f = Submodule.map f I.

LaTeX

$$$f : R \to S\, [h : \mathrm{RingHomSurjective} f] \Rightarrow \mathrm{Ideal.map} f I = \mathrm{Submodule.map} f^{\mathrm{toSemilinearMap}} I$$$

Lean4

instance (priority := low) (f : R →+* S) [RingHomSurjective f] (I : Ideal R) [I.IsTwoSided] : (I.map f).IsTwoSided where
  mul_mem_of_left b
    ha := by
    rw [map_eq_submodule_map] at ha ⊢
    obtain ⟨a, ha, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := f.surjective b
    rw [RingHom.coe_toSemilinearMap, ← map_mul]
    exact ⟨_, I.mul_mem_right _ ha, rfl⟩

Похожие утверждения