English
There exists a lower adjoint to the UniformFun.filter operation, establishing a Galois connection between filters. Concretely, for every filters 𝒜 and 𝓕, 𝒜 ≤ UniformFun.filter α β 𝓕 if and only if lowerAdjoint 𝒜 ≤ 𝓕; more generally, for any f : γ → α and any 𝓕, l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕).
Русский
Существует нижний сопряжённый оператор к операции UniformFun.filter, образующий отношение Галуа между фильтрами. Конкретно, для любых фильтров 𝒜 и 𝓕 выполняется 𝒜 ≤ UniformFun.filter α β 𝓕 тогда и только тогда, когда lowerAdjoint 𝒜 ≤ 𝓕; более общо, для любого f : γ → α и любого 𝓕 выполняется l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕).
LaTeX
$$$\forall \mathcal A, \mathcal F,\; \mathcal A \le \mathrm{UniformFun.filter}(\alpha,\beta)\,\mathcal F \iff \mathrm{lowerAdjoint}\,\mathcal A \le \mathcal F\\[5pt] \text{and for all } f: \gamma \to \alpha, \; l(\mathrm{Filter.map}(\mathrm{Prod.map} f f)\,\mathcal F) = \mathrm{Filter.map}(\mathrm{Prod.map} (f \circ) (f \circ))\, (l\,\mathcal F).$$
Lean4
/-- The function `UniformFun.filter α β : Filter (β × β) → Filter ((α →ᵤ β) × (α →ᵤ β))`
has a lower adjoint `l` (in the sense of `GaloisConnection`). The exact definition of `l` is not
interesting; we will only use that it exists (in `UniformFun.mono` and
`UniformFun.iInf_eq`) and that
`l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕)` for each
`𝓕 : Filter (γ × γ)` and `f : γ → α` (in `UniformFun.comap_eq`). -/
protected theorem gc : GaloisConnection lowerAdjoint fun 𝓕 => UniformFun.filter α β 𝓕 :=
by
intro 𝓐 𝓕
symm
calc
𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
_ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
_ ↔ ∀ U ∈ 𝓕, {uv | ∀ x, (uv, x) ∈ {t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U}} ∈ 𝓐 := Iff.rfl
_ ↔ ∀ U ∈ 𝓕, {uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U} ∈ 𝓐 ×ˢ (⊤ : Filter α) :=
(forall₂_congr fun U _hU => mem_prod_top.symm)
_ ↔ lowerAdjoint 𝓐 ≤ 𝓕 := Iff.rfl
