English
The restriction from the locale X into a sublocale is a nucleus on X.
Русский
Ограничение локали X к подлокали образует ядро на X.
LaTeX
$$$\text{toNucleus}(S) \text{ is a nucleus on } X$$$
Lean4
/-- The restriction from a locale X into the sublocale S. -/
def restrict (S : Sublocale X) : FrameHom X S
where
toFun x := sInf {s : S | x ≤ s}
map_inf' a
b := by
change Sublocale.restrictAux S (a ⊓ b) = Sublocale.restrictAux S a ⊓ Sublocale.restrictAux S b
refine eq_of_forall_ge_iff (fun s ↦ Iff.symm ?_)
calc
_ ↔ S.restrictAux a ≤ S.restrictAux b ⇨ s := by simp
_ ↔ S.restrictAux b ≤ a ⇨ s := by rw [S.giAux.gc.le_iff_le, @le_himp_comm, coe_himp]
_ ↔ b ≤ a ⇨ s := by
set c : S := ⟨a ⇨ s, S.himp_mem s.coe_prop⟩
change Sublocale.restrictAux S b ≤ c.val ↔ b ≤ c
rw [S.giAux.u_le_u_iff, S.giAux.gc.le_iff_le]
_ ↔ S.restrictAux (a ⊓ b) ≤ s := by simp [inf_comm, S.giAux.gc.le_iff_le]
map_sSup'
s := by
change Sublocale.restrictAux S (sSup s) = _
rw [S.giAux.gc.l_sSup, sSup_image]
rfl
map_top' := by
refine le_antisymm le_top ?_
change _ ≤ restrictAux S ⊤
rw [← Subtype.coe_le_coe, S.giAux.gc.u_top]
simp [restrictAux, sInf]
