English
Given a cover of a scheme by a precovering property, one can construct a new cover by reindexing, with a corresponding family of morphisms and identifications, and the new cover is again a valid cover in the same precoverage.
Русский
Дано покрытие схемы предпокрытием; можно построить новое покрытие путём перенумеровки, с соответствующими отображениями и идентификациями, и новое покрытие остаётся действительным в том же предпокрытии.
LaTeX
$$$\text{copy}: \text{X.Cover}(\text{precoverage } P) \to \text{X.Cover}(\text{precoverage } P)$ with data (J, obj, map, e1, e2, h) yielding a new cover with I0 := J, X := obj, f := map, and the isomorphisms e1,e2 satisfying compatibility h.$$
Lean4
/-- We construct a cover from another, by providing the needed fields and showing that the
provided fields are isomorphic with the original cover. -/
@[simps I₀ X f]
def copy [P.RespectsIso] {X : Scheme.{u}} (𝒰 : X.Cover (precoverage P)) (J : Type*) (obj : J → Scheme)
(map : ∀ i, obj i ⟶ X) (e₁ : J ≃ 𝒰.I₀) (e₂ : ∀ i, obj i ≅ 𝒰.X (e₁ i)) (h : ∀ i, map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)) :
X.Cover (precoverage P) where
I₀ := J
X := obj
f := map
mem₀ := by
rw [presieve₀_mem_precoverage_iff]
refine ⟨fun x ↦ ?_, ?_⟩
· obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
obtain ⟨i, rfl⟩ := e₁.surjective i
use i, (e₂ i).inv.base y
simp [h]
· simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]
intro i
exact 𝒰.map_prop _
