map — Mathlib

English

If I is fractional on S, then its pushforward along a morphism g remains fractional on the target.

Русский

Если I дробный на S, то его образ под линейным отображением g остаётся дробным на целевой области.

LaTeX

$$IsFractional S I → IsFractional S (Submodule.map g.toLinearMap I)$$

Lean4

theorem _root_.IsFractional.map (g : P →ₐ[R] P') {I : Submodule R P} :
    IsFractional S I → IsFractional S (Submodule.map g.toLinearMap I)
  | ⟨a, a_nonzero, hI⟩ =>
    ⟨a, a_nonzero, fun b hb => by
      obtain ⟨b', b'_mem, hb'⟩ := Submodule.mem_map.mp hb
      rw [AlgHom.toLinearMap_apply] at hb'
      obtain ⟨x, hx⟩ := hI b' b'_mem
      use x
      rw [← g.commutes, hx, map_smul, hb']⟩

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