English
There is a Galois coinsertion between the poset of ideal data and the poset of arbitrary families of ideals, realized by the two maps ideal and ofIdeals.
Русский
Существует Галуа-коинсерция между частично упорядоченными множествами данных идеалов и произвольных семей идеалов, реализованная парами отображений ideal и ofIdeals.
LaTeX
$$$\text{gci}: \mathrm{GaloisCoinsertion}(\text{ideal}, \operatorname{ofIdeals}(X))$$$
Lean4
/-- The Galois coinsertion between ideal sheaves and arbitrary families of ideals. -/
protected def gci : GaloisCoinsertion ideal (ofIdeals (X := X))
where
choice I
hI :=
{ ideal := I
map_ideal_basicOpen U f := (ideal_ofIdeals_le I).antisymm hI ▸ (ofIdeals I).map_ideal_basicOpen U f }
gc _ _ := ⟨(le_sSup ·), (le_trans · (ideal_ofIdeals_le _))⟩
u_l_le _ := sSup_le fun _ ↦ id
choice_eq I hI := IdealSheafData.ext (hI.antisymm (ideal_ofIdeals_le I))
