biSup_comap_eq_top_of_range_eq_biSup

English

If f is surjective, then the join of comap f p_i over i ∈ s equals top when the join of p_i is top.

Русский

Если f сюръективно, то свод comap f p_i по i в s равен верхней границе при условии, что ⋁ p_i = top.

LaTeX

$$$\bigvee_{i\in s} (p_i).comap f = \top$$$

Lean4

theorem biSup_comap_eq_top_of_range_eq_biSup {R R₂ : Type*} [Semiring R] [Ring R₂] {τ₁₂ : R →+* R₂}
    [RingHomSurjective τ₁₂] [Module R M] [Module R₂ M₂] {ι : Type*} (s : Set ι) (hs : s.Nonempty)
    (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
    ⨆ i ∈ s, (p i).comap f = ⊤ :=
  by
  suffices ⨆ i ∈ s, (p i).comap (LinearMap.range f).subtype = ⊤ by
    rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]; rfl
  exact hf ▸ biSup_comap_subtype_eq_top s p

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