English
If f: X → Y is induced and has closed range, then f is affine.
Русский
Если f индукционный и диапазон замкнут, то f аффинная.
LaTeX
$$$[Topology.IsInducing f.base] \\land [IsClosed (Set.range f.base)] \\Rightarrow IsAffineHom f$$$
Lean4
/-- If the underlying map of a morphism is inducing and has closed range, then it is affine. -/
@[stacks 04DE]
theorem isAffineHom_of_isInducing (hf₁ : Topology.IsInducing f.base) (hf₂ : IsClosed (Set.range f.base)) :
IsAffineHom f := by
apply isAffineHom_of_forall_exists_isAffineOpen
intro y
by_cases hy : y ∈ Set.range f.base
· obtain ⟨x, rfl⟩ := hy
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
(isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ (f.base x)) isOpen_univ
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen
obtain ⟨U', hU'U, rfl⟩ : ∃ U' : Y.Opens, U' ≤ U ∧ f ⁻¹ᵁ U' = V :=
by
obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩
obtain ⟨r, hrU', hxr⟩ := hU.exists_basicOpen_le ⟨f.base x, hxV⟩ hxU
refine ⟨_, hxr, hU.basicOpen r, ?_⟩
convert hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r)) using 1
simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]
simpa using ((Opens.map f.base).map (homOfLE hrU')).le
· obtain ⟨_, ⟨U, hU, rfl⟩, hyU, hU'⟩ := (isBasis_affine_open Y).exists_subset_of_mem_open hy hf₂.isOpen_compl
rw [Set.subset_compl_iff_disjoint_right, ← Set.preimage_eq_empty_iff] at hU'
refine ⟨U, hyU, hU, ?_⟩
convert isAffineOpen_bot _
exact Opens.ext hU'
