English
There exists an affine open neighborhood keeping the property P favorable under restriction.
Русский
Существует аффинное открытое окрестность, сохраняющее свойство P при ограничении.
LaTeX
$$∃ U', V' with P on restriction$$
Lean4
/-- If `P` holds for `f` over affine opens `U₂` of `Y` and `V₂` of `X` and `U₁` (resp. `V₁`) are
open neighborhoods of `x` (resp. `f.base x`), then `P` also holds for `f` over some affine open
`U'` of `Y` (resp. `V'` of `X`) that is contained in `U₁` (resp. `V₁`). -/
theorem exists_affineOpens_le_appLE_of_appLE (hPa : StableUnderCompositionWithLocalizationAwayTarget P)
(hPl : LocalizationAwayPreserves P) (x : X) (U₁ : Y.Opens) (U₂ : Y.affineOpens) (V₁ : X.Opens) (V₂ : X.affineOpens)
(hx₁ : x ∈ V₁) (hx₂ : x ∈ V₂.1) (e₂ : V₂.1 ≤ f ⁻¹ᵁ U₂.1) (h₂ : P (f.appLE U₂ V₂ e₂).hom) (hfx₁ : f.base x ∈ U₁.1) :
∃ (U' : Y.affineOpens) (V' : X.affineOpens) (_ : U'.1 ≤ U₁) (_ : V'.1 ≤ V₁) (_ : x ∈ V'.1) (e : V'.1 ≤ f ⁻¹ᵁ U'.1),
P (f.appLE U' V' e).hom :=
by
obtain ⟨r, hBr, hBfx⟩ := U₂.2.exists_basicOpen_le ⟨f.base x, hfx₁⟩ (e₂ hx₂)
obtain ⟨s, hBs, hBx⟩ := V₂.2.exists_basicOpen_le ⟨x, hx₁⟩ hx₂
obtain ⟨r', s', hBx', e', hf'⟩ :=
exists_basicOpen_le_appLE_of_appLE_of_isAffine hPa hPl x ⟨Y.basicOpen r, U₂.2.basicOpen _⟩ U₂
⟨X.basicOpen s, V₂.2.basicOpen _⟩ V₂ hBx hx₂ e₂ h₂ hBfx
exact
⟨⟨Y.basicOpen r', (U₂.2.basicOpen _).basicOpen _⟩, ⟨X.basicOpen s', (V₂.2.basicOpen _).basicOpen _⟩,
le_trans (Y.basicOpen_le _) hBr, le_trans (X.basicOpen_le _) hBs, hBx', e', hf'⟩
