The radical of a lattice

This file contains results on the order radical of a lattice: the infimum of the coatoms.

def Order.radical (α : Type u_1) [Preorder α] [OrderTop α] [InfSet α] : α

The infimum of all coatoms.

This notion specializes, e.g. in the subgroup lattice of a group to the Frattini subgroup, or in the lattices of ideals in a ring R to the Jacobson ideal.

Equations

• Order.radical α = ⨅ a ∈ {H : α | IsCoatom H}, a

theorem Order.radical_le_coatom {α : Type u_1} [CompleteLattice α] {a : α} (h : IsCoatom a) : Order.radical α ≤ a

theorem OrderIso.map_radical {α : Type u_1} [CompleteLattice α] {β : Type u_2} [CompleteLattice β] (f : α ≃o β) : f (Order.radical α) = Order.radical β

theorem Order.radical_nongenerating {α : Type u_1} [CompleteLattice α] [IsCoatomic α] {a : α} (h : a ⊔ Order.radical α = ⊤) : a = ⊤