comap_iInf — Mathlib

English

When f is surjective, comap commutes with arbitrary infima: comap f (⨅ i, p_i) = ⨅ i, comap f (p_i).

Русский

При сюръективности f предобраз сохраняет произвольные INF: comap f (⋂_i p_i) = ⋂_i comap f(p_i).

LaTeX

$$$\operatorname{comap} f \left( \bigsqcap_{i} p_i \right) = \bigsqcap_{i} \operatorname{comap} f (p_i)$$$

Lean4

@[simp]
theorem comap_iInf [RingHomSurjective σ₁₂] {ι : Sort*} (f : F) (p : ι → Submodule R₂ M₂) :
    comap f (⨅ i, p i) = ⨅ i, comap f (p i) :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).u_iInf

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