isSMulRegular_on_quot_iff_smul_top_inf_eq_smul

English

If r is regular on M, then IsSMulRegular on M/N is equivalent to a top-inf inequality: r · ⊤ ∩ N ≤ r · N.

Русский

Если r регулярен на M, то IsSMulRegular на M/N эквивалентна неравенству: r · ⊤ ∩ N ≤ r · N.

LaTeX

$$$IsSMulRegular(M,r) \Rightarrow (IsSMulRegular(M/N,r) \iff r \cdot \top \cap N \le r \cdot N)$$$

Lean4

theorem isSMulRegular_on_quot_iff_smul_top_inf_eq_smul :
    IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N) :=
  by
  intro (h : Function.Injective (DistribMulAction.toLinearMap R M r))
  rw [isSMulRegular_on_quot_iff_lsmul_comap_le, ← map_le_map_iff_of_injective h, ←
    LinearMap.lsmul_eq_DistribMulAction_toLinearMap, map_comap_eq, LinearMap.range_eq_map];
  rfl

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