English
The units in the stalk of smooth functions are characterized by nonvanishing at the point x.
Русский
Единицы в stalk непрерывных функций — это латентные элементы, не обращающиеся в нуль на точке x.
LaTeX
$$isUnit_stalk {x} f : IsUnit f ↔ f ∉ ker (smoothSheafCommRing.eval x)$$
Lean4
/-- The units of the stalk at `x` of the sheaf of smooth functions from `M` to `𝕜`, considered as a
sheaf of commutative rings, are the functions whose values at `x` are nonzero. -/
theorem isUnit_stalk_iff {x : M} (f : (smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf.stalk x) :
IsUnit f ↔ f ∉ RingHom.ker (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x) :=
by
constructor
· rintro ⟨⟨f, g, hf, hg⟩, rfl⟩ (h' : smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x f = 0)
simpa [h'] using congr_arg (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x) hf
· let S := (smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf
rintro
(hf : _ ≠ 0)
-- Represent `f` as the germ of some function (also called `f`) on an open neighbourhood `U` of
-- `x`, which is nonzero at `x`
obtain ⟨U : Opens M, hxU, f : C^∞⟮IM, U; 𝓘(𝕜), 𝕜⟯, rfl⟩ := S.germ_exist x f
have hf' : f ⟨x, hxU⟩ ≠ 0 := by
convert hf
exact (smoothSheafCommRing.eval_germ U x hxU f).symm
have H : ∀ᶠ (z : U) in 𝓝 ⟨x, hxU⟩, f z ≠ 0 := f.2.continuous.continuousAt.eventually_ne hf'
rw [eventually_nhds_iff] at H
obtain ⟨V₀, hV₀f, hV₀, hxV₀⟩ := H
let V : Opens M := ⟨Subtype.val '' V₀, U.2.isOpenMap_subtype_val V₀ hV₀⟩
have hUV : V ≤ U := Subtype.coe_image_subset (U : Set M) V₀
have hV : V₀ = Set.range (Set.inclusion hUV) :=
by
convert (Set.range_inclusion hUV).symm
ext y
change _ ↔ y ∈ Subtype.val ⁻¹' (Subtype.val '' V₀)
rw [Set.preimage_image_eq _ Subtype.coe_injective]
clear_value V
subst hV
have hxV : x ∈ (V : Set M) := by
obtain ⟨x₀, hxx₀⟩ := hxV₀
convert x₀.2
exact congr_arg Subtype.val hxx₀.symm
have hVf : ∀ y : V, f (Set.inclusion hUV y) ≠ 0 := fun y ↦
hV₀f (Set.inclusion hUV y)
(Set.mem_range_self y)
-- Let `g` be the pointwise inverse of `f` on `V`, which is smooth since `f` is nonzero there
let g : C^∞⟮IM, V; 𝓘(𝕜), 𝕜⟯ :=
⟨(f ∘ Set.inclusion hUV)⁻¹, ?_⟩
-- The germ of `g` is inverse to the germ of `f`, so `f` is a unit
· refine
⟨⟨S.germ _ x (hxV) (ContMDiffMap.restrictRingHom IM 𝓘(𝕜) 𝕜 hUV f), S.germ _ x hxV g, ?_, ?_⟩,
S.germ_res_apply hUV.hom x hxV f⟩
· rw [← map_mul]
-- Qualified the name to avoid Lean not finding a `OneHomClass` https://github.com/leanprover-community/mathlib4/pull/8386
convert RingHom.map_one _
apply Subtype.ext
ext y
apply mul_inv_cancel₀
exact hVf y
· rw [← map_mul]
-- Qualified the name to avoid Lean not finding a `OneHomClass` https://github.com/leanprover-community/mathlib4/pull/8386
convert RingHom.map_one _
apply Subtype.ext
ext y
apply inv_mul_cancel₀
exact hVf y
· intro y
exact (((contDiffAt_inv _ (hVf y)).contMDiffAt).comp y (f.contMDiff.comp (contMDiff_inclusion hUV)).contMDiffAt :)
