AlgebraicGeometry.IsClosedImmersion.app_injective_and_exists_of_app_pullback_eq_of_isReduced
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.IsClosedImmersion
universe u
open _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometryLean source · full declaration
theorem app_injective_and_exists_of_app_pullback_eq_of_isReduced
{X Y₁ Y₂ : Scheme.{u}} [IsReduced X] (i₁ : Y₁ ⟶ X) (i₂ : Y₂ ⟶ X)
[IsClosedImmersion i₁] [IsClosedImmersion i₂]
(hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
(U : X.Opens) :
Function.Injective (fun f : Γ(X, U) => ((i₁.app U) f, (i₂.app U) f)) ∧
∀ (g₁ : Γ(Y₁, i₁ ⁻¹ᵁ U)) (g₂ : Γ(Y₂, i₂ ⁻¹ᵁ U)),
(pullback i₁ i₂).presheaf.map
(eqToHom (show (pullback.snd i₁ i₂) ⁻¹ᵁ (i₂ ⁻¹ᵁ U) = (pullback.fst i₁ i₂) ⁻¹ᵁ (i₁ ⁻¹ᵁ
U) by
rw [← Scheme.Hom.comp_preimage, ← Scheme.Hom.comp_preimage, pullback.condition])).op
((pullback.fst i₁ i₂).app (i₁ ⁻¹ᵁ U) g₁) =
(pullback.snd i₁ i₂).app (i₂ ⁻¹ᵁ U) g₂ →
∃ f : Γ(X, U), (i₁.app U) f = g₁ ∧ (i₂.app U) f = g₂ := by
exact AlgebraicGeometry.Scheme.Hom.app_injective_and_exists_of_forall_isAffineOpen i₁ i₂ U
(fun V hV _ => app_injective_and_exists_of_app_pullback_eq_of_isAffineOpen
i₁ i₂ hcover V hV)