English
In a complemented modular lattice that is compactly generated, the lattice is atomic.
Русский
В комплементированной модульной решётке, которая компактно порождаема, решётка атомистична.
LaTeX
$$$ \text{IsAtomic}(\mathcal{A}) $ where $\mathcal{A}$ is complemented and modular and compactly generated$$
Lean4
/-- A compact element `k` has the property that any `b < k` lies below a "maximal element below
`k`", which is to say `[⊥, k]` is coatomic. -/
theorem Iic_coatomic_of_compact_element {k : α} (h : IsCompactElement k) : IsCoatomic (Set.Iic k) :=
by
constructor
rintro ⟨b, hbk⟩
obtain rfl | H := eq_or_ne b k
· left; ext; simp only [Set.Iic.coe_top]
right
have ⟨a, ba, h⟩ := zorn_le_nonempty₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)
· refine ⟨⟨a, le_of_lt h.prop⟩, ⟨ne_of_lt h.prop, fun c hck => by_contradiction fun c₀ => ?_⟩, ba⟩
cases h.eq_of_le (y := c.1) (lt_of_le_of_ne c.2 fun con ↦ c₀ (Subtype.ext con)) hck.le
exact lt_irrefl _ hck
· intro S SC cC I _
by_cases hS : S.Nonempty
· refine ⟨sSup S, h.directed_sSup_lt_of_lt hS cC.directedOn SC, ?_⟩
intro; apply le_sSup
exact
⟨b, lt_of_le_of_ne hbk H, by
simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
not_false_iff]⟩
