English
A symmetry lemma asserting equality of two ways to realize an open cover from the irrelevance data.
Русский
Лемма симметрии, утверждающая равенство разных способов реализации открытого покрытия из данных нерелевантности.
LaTeX
$$$Eq\\_1\\left( openCoverOfMapIrrelevantEqTop \\right)$$$
Lean4
/-- Given a family of homogeneous elements `f` of positive degree that spans the irrelevant ideal,
`Spec (A_f)₀ ⟶ Proj A` forms an affine open cover of `Proj A`. -/
noncomputable def affineOpenCoverOfIrrelevantLESpan {ι : Type*} (f : ι → A) {m : ι → ℕ} (f_deg : ∀ i, f i ∈ 𝒜 (m i))
(hm : ∀ i, 0 < m i) (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)) :
(Proj 𝒜).AffineOpenCover where
I₀ := ι
X i := .of (Away 𝒜 (f i))
f i := awayι 𝒜 (f i) (f_deg i) (hm i)
idx x := (mem_iSup.mp ((iSup_basicOpen_eq_top 𝒜 f hf).ge (Set.mem_univ x))).choose
covers
x := by
change x ∈ (awayι 𝒜 _ _ _).opensRange
rw [opensRange_awayι]
exact (mem_iSup.mp ((iSup_basicOpen_eq_top 𝒜 f hf).ge (Set.mem_univ x))).choose_spec
