AlgebraicGeometry.Scheme.OrderedAffineCover.exists_refinement_preimage_preimage_of_isSeparated
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_OrderedAffineCover_exists_refinement_preimage_preimage_of_isSeparated in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry inLean source · statement
theorem exists_refinement_preimage_preimage_of_isSeparated
{R : Type} [CommRing R] {X : Scheme.{0}} (f : X ⟶ Spec (CommRingCat.of R)) [IsSeparated f]
(𝒦 : X.OrderedAffineCover) (h₁ h₂ : X ⟶ X) [IsAffineHom h₁] [IsAffineHom h₂] :
∃ (𝒲 : X.OrderedAffineCover) (lam₁ lam₂ : 𝒲.ι → 𝒦.ι),
(∀ w, 𝒲.U w ≤ h₁ ⁻¹ᵁ 𝒦.U (lam₁ w)) ∧ (∀ w, 𝒲.U w ≤ h₂ ⁻¹ᵁ 𝒦.U (lam₂ w))