English
For a map φ, the closure of s ∩ ker φ equals closure s intersect ker φ.
Русский
Для отображения φ, замыкание s ∩ ker φ равно замыканию s пересеченному с ker φ.
LaTeX
$$$\overline{s \cap \ker \phi} = \overline{s} \cap \ker \phi.$$$
Lean4
theorem closure_ker_inter {F S K A : Type*} [CommRing K] [Ring A] [Algebra K A] [TopologicalSpace K] [T1Space K]
[TopologicalSpace A] [ContinuousSub A] [ContinuousSMul K A] [FunLike F A K] [AlgHomClass F K A K] [SetLike S A]
[OneMemClass S A] [AddSubgroupClass S A] [SMulMemClass S K A] (φ : F) (hφ : Continuous φ) (s : S) :
closure (s ∩ RingHom.ker φ) = closure s ∩ (ker φ : Set A) :=
by
refine subset_antisymm ?_ ?_
·
simpa only [ker_eq, (isClosed_singleton.preimage hφ).closure_eq] using
closure_inter_subset_inter_closure s (ker φ : Set A)
· intro x ⟨hxs, (hxφ : φ x = 0)⟩
rw [mem_closure_iff_clusterPt, ClusterPt] at hxs
have : Tendsto (fun y ↦ y - φ y • 1) (𝓝 x ⊓ 𝓟 s) (𝓝 x) :=
by
conv => congr; rfl; rfl; rw [← sub_zero x, ← zero_smul K 1, ← hxφ]
exact Filter.tendsto_inf_left (Continuous.tendsto (by fun_prop) x)
refine mem_closure_of_tendsto this <| eventually_inf_principal.mpr ?_
filter_upwards [] with g hg using ⟨sub_mem hg (SMulMemClass.smul_mem _ <| one_mem _), by simp [RingHom.mem_ker]⟩
