AlgebraicGeometry.Scheme.OrderedAffineCover.exists_refinement_pullback_fst_snd_of_isSeparated
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open Scheme_OrderedAffineCover_exists_refinement_pullback_fst_snd_of_isSeparated in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in
open _root_.AlgebraicGeometry.Scheme.Pullback inLean source · statement
theorem exists_refinement_pullback_fst_snd_of_isSeparated
{R : Type u} [CommRing R] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of R)) [IsSeparated f]
(𝒦 : A.OrderedAffineCover) (μ : pullback f f ⟶ A) (_hμ : μ ≫ f = pullback.fst f f ≫ f) :
∃ (𝒲 : (pullback f f).OrderedAffineCover) (lam₁ lam₂ lam₃ : 𝒲.ι → 𝒦.ι),
(∀ w, 𝒲.U w ≤ pullback.fst f f ⁻¹ᵁ 𝒦.U (lam₁ w)) ∧
(∀ w, 𝒲.U w ≤ pullback.snd f f ⁻¹ᵁ 𝒦.U (lam₂ w)) ∧
(∀ w, 𝒲.U w ≤ μ ⁻¹ᵁ 𝒦.U (lam₃ w))