Scheme_exists_isOpenImmersion_of_functionField_iso.lean

theorem isOpenImmersion_ι_comp_of_inverse_on_opens {X Y : Scheme.{u}} (f : X ⟶ Y)
    (B : Y.Opens) (gB : (B : Scheme.{u}) ⟶ X)
    (W : X.Opens) (hWB : W ≤ f ⁻¹ᵁ B) (hb : f.resLE B W hWB ≫ gB = W.ι)
    (W' : Y.Opens) (hW'B : W' ≤ B) (ha : Y.homOfLE hW'B ≫ gB ≫ f = W'.ι) :
    IsOpenImmersion ((W ⊓ f ⁻¹ᵁ W').ι ≫ f)

theorem Scheme.Opens.fromSpecStalk_comp_eq {X Y : Scheme.{u}} (U : X.Opens) {x : X} (hx : x ∈ U)
    {k₁ k₂ : (U : Scheme.{u}) ⟶ Y}
    (h : U.fromSpecStalkOfMem x hx ≫ k₁ = U.fromSpecStalkOfMem x hx ≫ k₂) :
    (U : Scheme.{u}).fromSpecStalk ⟨x, hx⟩ ≫ k₁ = (U : Scheme.{u}).fromSpecStalk ⟨x, hx⟩ ≫ k₂

theorem isOpenImmersion_ι_comp_of_inverse_on_opens' {X Y : Scheme.{u}} (f : X ⟶ Y)
    (B : Y.Opens) (gB : (B : Scheme.{u}) ⟶ X)
    (W₀ : (f ⁻¹ᵁ B : Scheme.{u}).Opens)
    (hb₀ : W₀.ι ≫ f.resLE B (f ⁻¹ᵁ B) le_rfl ≫ gB = W₀.ι ≫ (f ⁻¹ᵁ B).ι)
    (W'₀ : (B : Scheme.{u}).Opens) (ha₀ : W'₀.ι ≫ gB ≫ f = W'₀.ι ≫ B.ι) :
    IsOpenImmersion ((((f ⁻¹ᵁ B).ι ''ᵁ W₀) ⊓ f ⁻¹ᵁ (B.ι ''ᵁ W'₀)).ι ≫ f)

theorem _root_.AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_eq_of_eq {X : Scheme.{u}}
  (U : X.Opens) {y y' : X}
    (e : y = y') (hy : y ∈ U) (hy' : y' ∈ U) :
    U.fromSpecStalkOfMem y hy =
      Spec.map (X.presheaf.stalkSpecializes (specializes_of_eq e)) ≫ U.fromSpecStalkOfMem y' hy'

theorem Scheme.Opens.fromSpecStalkOfMem_resLE {X Y : Scheme.{u}} (k : X ⟶ Y) (U : Y.Opens) (x : X)
    (hx : x ∈ k ⁻¹ᵁ U) :
    (k ⁻¹ᵁ U).fromSpecStalkOfMem x hx ≫ k.resLE U (k ⁻¹ᵁ U) le_rfl =
      Spec.map (k.stalkMap x) ≫ U.fromSpecStalkOfMem (k.base x) hx

theorem Scheme.b1_main
    {K : Type u} [Field K] {C C' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (c' : C' ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsIntegral C'] [LocallyOfFiniteType c] [LocallyOfFiniteType c']
    (ψ : C.functionField ≅ C'.functionField)
    (hψ : Spec.map ψ.inv ≫ C'.fromSpecStalk (genericPoint C') ≫ c' =
      C.fromSpecStalk (genericPoint C) ≫ c) :
    ∃ (U : C.Opens) (hη : genericPoint C ∈ U) (j : (U : Scheme.{u}) ⟶ C') (_ : IsOpenImmersion j),
      j ≫ c' = U.ι ≫ c ∧
      U.fromSpecStalkOfMem (genericPoint C) hη ≫ j =
        Spec.map ψ.inv ≫ C'.fromSpecStalk (genericPoint C')

theorem _root_.AlgebraicGeometry.Scheme.exists_isOpenImmersion_of_functionField_iso
    {K : Type u} [Field K] {C C' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (c' : C' ⟶ Spec (CommRingCat.of K))
    [IsIntegral C] [IsIntegral C'] [LocallyOfFiniteType c] [LocallyOfFiniteType c']
    (ψ : C.functionField ≅ C'.functionField)
    (hψ : Spec.map ψ.inv ≫ C'.fromSpecStalk (genericPoint C') ≫ c' =
      C.fromSpecStalk (genericPoint C) ≫ c) :
    ∃ (U : C.Opens) (hη : genericPoint C ∈ U) (j : (U : Scheme.{u}) ⟶ C') (_ : IsOpenImmersion j),
      j ≫ c' = U.ι ≫ c ∧
      U.fromSpecStalkOfMem (genericPoint C) hη ≫ j =
        Spec.map ψ.inv ≫ C'.fromSpecStalk (genericPoint C')