NYLL
Module

exists_fg_subalgebra_isPullback_of_iSup_eq_top_of_locallyOfFinitePresentation.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_fg_subalgebra_isPullback_of_iSup_eq_top_of_locallyOfFinitePresentation
32 declarations indexed from sourceView source ↗

Module documentation

Descent of a scheme obtained by gluing two quasi-compact open models

Imports6
Imported by2

Declarations

abbrev

ι

L57 ↗
UnionModel.ι
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
Lean source · statement
abbrev _root_.UnionModel.ι (A B : Type u) [CommRing A] [CommRing B] [Algebra
  B A] :
    Spec (CommRingCat.of A) ⟶ Spec (CommRingCat.of B)
theorem

ι_comp

L65 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.ι_comp
Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
omit [CommRing A] in
Lean source · statement
theorem ι_comp (A : Type u) [CommRing A] (B : Type u) [CommRing B] [Algebra B A] (B' : Type u)
  [CommRing B'] [Algebra B' A]
    (φ : B →+* B') (hφ : (algebraMap B' A).comp φ = algebraMap B A) :
    ι A B' ≫ Spec.map (CommRingCat.ofHom φ) = ι A B
structure

Model

L72 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model
Documentation

A finitely presented model together with its base-change identification.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
Lean source · full declaration
structure Model (B : Type u) [CommRing B] [Algebra B A] {Y : Scheme.{u}} (gY : Y ⟶ Spec
  (CommRingCat.of A)) where
  /-- The scheme over the smaller coefficient ring. -/
  X₀ : Scheme.{u}
  /-- The structure morphism of the model. -/
  f₀ : X₀ ⟶ Spec (CommRingCat.of B)
  /-- The comparison morphism from the original scheme. -/
  π : Y ⟶ X₀
  /-- Finite presentation of the structure morphism. -/
  lfp : LocallyOfFinitePresentation f₀
  /-- Quasi-compactness of the structure morphism. -/
  qc : QuasiCompact f₀
  /-- Quasi-separatedness of the structure morphism. -/
  qs : QuasiSeparated f₀
  /-- The square identifying the original scheme with the base change. -/
  sq : IsPullback π gY f₀ (ι A B)
def

q

L100 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.q
Documentation

The comparison between the two pullbacks after extending coefficients.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
def q : pullback M.f₀ (ι A B) ⟶ pullback M.f₀ (Spec.map (CommRingCat.ofHom φ))
theorem

q_fst

L104 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.q_fst
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem q_fst : M.q B' φ hφ ≫ pullback.fst _ _ = pullback.fst _ _
theorem

q_snd

L106 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.q_snd
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem q_snd : M.q B' φ hφ ≫ pullback.snd _ _ = pullback.snd _ _ ≫ ι A B'
def

map

L110 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.map
Documentation

Extension of the coefficient ring of a model.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · full declaration
def map : Model B' gY where
  X₀ := pullback M.f₀ (Spec.map (CommRingCat.ofHom φ))
  f₀ := pullback.snd _ _
  π := M.sq.isoPullback.hom ≫ M.q B' φ hφ
  lfp := inferInstance
  qc := inferInstance
  qs := inferInstance
  sq := by
    have h1 : IsPullback (M.q B' φ hφ) (pullback.snd M.f₀ (ι A B))
        (pullback.snd M.f₀ (Spec.map (CommRingCat.ofHom φ))) (ι A B') := by
      refine IsPullback.of_right ?_ (M.q_snd B' φ hφ) (IsPullback.of_hasPullback _ _)
      rw [q_fst, ι_comp A B B' φ hφ]
      exact IsPullback.of_hasPullback _ _
    have h2 : IsPullback M.sq.isoPullback.hom (M.sq.isoPullback.hom ≫ pullback.snd M.f₀ (ι A B))
        (pullback.snd M.f₀ (ι A B)) (𝟙 _) :=
      IsPullback.of_horiz_isIso ⟨by rw [Category.comp_id]⟩
    have := h2.paste_horiz h1
    rw [Category.id_comp, IsPullback.isoPullback_hom_snd] at this
    exact this
theorem

map_X₀

L130 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.map_X₀
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem map_X₀ : (M.map B' φ hφ).X₀ = pullback M.f₀ (Spec.map (CommRingCat.ofHom φ))
theorem

map_f₀

L132 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.map_f₀
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem map_f₀ : (M.map B' φ hφ).f₀ = pullback.snd _ _
theorem

map_π

L133 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.map_π
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem map_π : (M.map B' φ hφ).π = M.sq.isoPullback.hom ≫ M.q B' φ hφ
theorem

map_π_fst

L135 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.map_π_fst
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem map_π_fst : (M.map B' φ hφ).π ≫ pullback.fst _ _ = M.π
theorem

map_π_snd

L140 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.map_π_snd
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem map_π_snd : (M.map B' φ hφ).π ≫ pullback.snd _ _ = gY ≫ ι A B'
theorem

map_π_preimage

L146 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.map_π_preimage
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem map_π_preimage (W₀ : M.X₀.Opens) :
    (M.map B' φ hφ).π ⁻¹ᵁ ((pullback.fst M.f₀ (Spec.map (CommRingCat.ofHom φ))) ⁻¹ᵁ W₀) = M.π ⁻¹ᵁ
      W₀
theorem

isCompact_fst_preimage

L153 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.isCompact_fst_preimage
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section map
variable (M : Model B gY) (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B')
  (hφ : (algebraMap B' A).comp φ = algebraMap B A)
Lean source · statement
theorem isCompact_fst_preimage (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀)) :
    IsCompact (((pullback.fst M.f₀ (Spec.map (CommRingCat.ofHom φ))) ⁻¹ᵁ W₀ : (M.map B' φ
      hφ).X₀.Opens) :
      Set ↥(M.map B' φ hφ).X₀)
theorem

range_subset

L177 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.range_subset
Source context 14 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section restrictOpen
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
include h in
Lean source · statement
theorem range_subset : Set.range (k ≫ M.π).base ⊆ Set.range W₀.ι.base
def

restrictOpen

L186 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.restrictOpen
Documentation

Restriction of a model to a compatible quasi-compact open.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section restrictOpen
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
Lean source · full declaration
def restrictOpen : Model B gW where
  X₀ := W₀
  f₀ := W₀.ι ≫ M.f₀
  π := IsOpenImmersion.lift W₀.ι (k ≫ M.π) (M.range_subset W₀ k h)
  lfp := inferInstance
  qc := by
    have : CompactSpace ↥W₀ := isCompact_iff_compactSpace.mp hc
    exact (quasiCompact_iff_compactSpace (W₀.ι ≫ M.f₀)).mpr ‹_›
  qs := inferInstance
  sq := by
    have top : IsPullback (IsOpenImmersion.lift W₀.ι (k ≫ M.π) (M.range_subset W₀ k h)) k W₀.ι M.π
      :=
      IsOpenImmersion.isPullback _ _ _ _ (IsOpenImmersion.lift_fac _ _ _).symm
        (by rw [Scheme.Opens.opensRange_ι]; exact h)
    rw [hgW]
    exact top.paste_vert M.sq
theorem

restrictOpen_X₀

L203 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.restrictOpen_X₀
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section restrictOpen
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
Lean source · statement
theorem restrictOpen_X₀ : (M.restrictOpen W₀ hc k h gW hgW).X₀ = W₀
theorem

restrictOpen_f₀

L204 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.restrictOpen_f₀
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section restrictOpen
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
Lean source · statement
theorem restrictOpen_f₀ : (M.restrictOpen W₀ hc k h gW hgW).f₀ = W₀.ι ≫ M.f₀
theorem

restrictOpen_π_ι

L205 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.restrictOpen_π_ι
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section restrictOpen
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
Lean source · statement
theorem restrictOpen_π_ι : (M.restrictOpen W₀ hc k h gW hgW).π ≫ W₀.ι = k ≫ M.π
abbrev

toStage

L214 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.toStage
Documentation

The model over an intermediate finitely generated subalgebra.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section dock
variable (M : Model B gY)
Lean source · statement
abbrev toStage (T' : Subalgebra B A) : Model ↥T' gY
theorem

exists_open

L217 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.exists_open
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section dock
variable (M : Model B gY)
Lean source · statement
theorem exists_open (W : Y.Opens) (hW : IsCompact (W : Set ↥Y)) (s : Finset A) :
    ∃ (T' : Subalgebra B A), T'.FG ∧ (↑s : Set A) ⊆ T' ∧
      ∃ W₀ : (M.toStage T').X₀.Opens, IsCompact (W₀ : Set ↥(M.toStage T').X₀) ∧ (M.toStage T').π
        ⁻¹ᵁ W₀ = W
theorem

exists_iso

L237 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.exists_iso
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section dock
variable (M : Model B gY)
Lean source · statement
theorem exists_iso (M₁ M₂ : Model B gY) (s : Finset A) :
    ∃ (T' : Subalgebra B A), T'.FG ∧ (↑s : Set A) ⊆ T' ∧
      ∃ e₀ : (M₁.toStage T').X₀ ≅ (M₂.toStage T').X₀,
        e₀.hom ≫ (M₂.toStage T').f₀ = (M₁.toStage T').f₀ ∧ (M₁.toStage T').π ≫ e₀.hom = (M₂.toStage
          T').π
def

inc

L271 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.inc
Documentation

The open immersion between base-changed models induced by restriction.

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
def inc :
    ((M.restrictOpen W₀ hc k h gW hgW).map B' φ hφ).X₀ ⟶ (M.map B' φ hφ).X₀
instance

(anonymous instance)

L276 ↗
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
instance : IsOpenImmersion (M.inc W₀ hc k h gW hgW B' φ hφ)
theorem

inc_fst

L282 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.inc_fst
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
theorem inc_fst : M.inc W₀ hc k h gW hgW B' φ hφ ≫ pullback.fst M.f₀ (Spec.map
  (CommRingCat.ofHom φ)) =
    pullback.fst (W₀.ι ≫ M.f₀) (Spec.map (CommRingCat.ofHom φ)) ≫ W₀.ι
theorem

inc_snd

L288 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.inc_snd
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
theorem inc_snd : M.inc W₀ hc k h gW hgW B' φ hφ ≫ pullback.snd M.f₀ (Spec.map
  (CommRingCat.ofHom φ)) =
    pullback.snd (W₀.ι ≫ M.f₀) (Spec.map (CommRingCat.ofHom φ))
theorem

inc_f₀

L294 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.inc_f₀
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
theorem inc_f₀ : M.inc W₀ hc k h gW hgW B' φ hφ ≫ (M.map B' φ hφ).f₀ =
    ((M.restrictOpen W₀ hc k h gW hgW).map B' φ hφ).f₀
theorem

inc_opensRange

L298 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.inc_opensRange
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
theorem inc_opensRange : (M.inc W₀ hc k h gW hgW B' φ hφ).opensRange =
    (pullback.fst M.f₀ (Spec.map (CommRingCat.ofHom φ))) ⁻¹ᵁ W₀
theorem

rmap_π_fst

L307 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.rmap_π_fst
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
theorem rmap_π_fst : ((M.restrictOpen W₀ hc k h gW hgW).map B' φ hφ).π ≫
    pullback.fst (W₀.ι ≫ M.f₀) (Spec.map (CommRingCat.ofHom φ)) = (M.restrictOpen W₀ hc k h gW
      hgW).π
theorem

rmap_π_snd

L312 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.rmap_π_snd
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
theorem rmap_π_snd : ((M.restrictOpen W₀ hc k h gW hgW).map B' φ hφ).π ≫
    pullback.snd (W₀.ι ≫ M.f₀) (Spec.map (CommRingCat.ofHom φ)) = gW ≫ ι A B'
theorem

sq_inc

L316 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model.sq_inc
Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
attribute [-instance] AlgebraicGeometry.SubalgebraStages.compactSpace_pullback
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_pullback
  AlgebraicGeometry.SubalgebraStages.compactSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiSeparatedSpace_obj
  AlgebraicGeometry.SubalgebraStages.quasiCompact_snd
  AlgebraicGeometry.SubalgebraStages.isAffineHom_leg
  AlgebraicGeometry.SubalgebraStages.isAffineHom_trans
  AlgebraicGeometry.SubalgebraStages.isAffineHom_diagram_map
  AlgebraicGeometry.SubalgebraStages.quasiSeparated_snd
  AlgebraicGeometry.SubalgebraStages.isCofiltered_op
attribute [-simp] AlgebraicGeometry.SubalgebraStages.specCone_π_app
  AlgebraicGeometry.SubalgebraStages.specLeg_specHom
  AlgebraicGeometry.SubalgebraStages.specLeg_specTrans AlgebraicGeometry.SubalgebraStages.cone_pt
  AlgebraicGeometry.SubalgebraStages.trans_fst AlgebraicGeometry.SubalgebraStages.diagram_obj
  AlgebraicGeometry.SubalgebraStages.leg_snd AlgebraicGeometry.SubalgebraStages.diagram_map
  AlgebraicGeometry.SubalgebraStages.specTrans_refl AlgebraicGeometry.SubalgebraStages.trans_snd
  AlgebraicGeometry.SubalgebraStages.specTrans_specHom
  AlgebraicGeometry.SubalgebraStages.specCone_pt AlgebraicGeometry.SubalgebraStages.cone_π_app
  AlgebraicGeometry.SubalgebraStages.specDiagram_map
  AlgebraicGeometry.SubalgebraStages.specDiagram_obj AlgebraicGeometry.SubalgebraStages.leg_fst
  AlgebraicGeometry.SubalgebraStages.leg_trans
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace UnionModel
variable {A : Type u} [CommRing A]
attribute [scoped instance] Model.lfp Model.qc Model.qs
namespace Model
variable {B : Type u} [CommRing B] [Algebra B A] {Y : Scheme.{u}} {gY : Y ⟶ Spec (CommRingCat.of A)}
section inc
variable (M : Model B gY) (W₀ : M.X₀.Opens) (hc : IsCompact (W₀ : Set ↥M.X₀))
  {W : Scheme.{u}} (k : W ⟶ Y) [IsOpenImmersion k] (h : M.π ⁻¹ᵁ W₀ = k.opensRange)
  (gW : W ⟶ Spec (CommRingCat.of A)) (hgW : gW = k ≫ gY)
  (B' : Type u) [CommRing B'] [Algebra B' A] (φ : B →+* B') (hφ : (algebraMap B' A).comp φ =
    algebraMap B A)
Lean source · statement
theorem sq_inc : IsPullback k ((M.restrictOpen W₀ hc k h gW hgW).map B' φ hφ).π (M.map B' φ hφ).π
    (M.inc W₀ hc k h gW hgW B' φ hφ)
theorem

exists_fg_subalgebra_isPullback_of_iSup_eq_top_of_locallyOfFinitePresentation

L398 ↗
AlgebraicGeometry.exists_fg_subalgebra_isPullback_of_iSup_eq_top_of_locallyOfFinitePresentation
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicGeometry
open scoped
  AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel.Model
open CategoryTheory CategoryTheory.Limits
open AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent
universe u
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs.UnionDescent.UnionModel UnionModel.Model
Lean source · statement
theorem exists_fg_subalgebra_isPullback_of_iSup_eq_top_of_locallyOfFinitePresentation
    {A₀ R A : Type u} [CommRing A₀] [CommRing R] [CommRing A] [Algebra A₀ R] [Algebra R A] [Algebra
      A₀ A]
    [IsScalarTower A₀ R A] [Algebra.FiniteType A₀ R]
    {X : Scheme.{u}} (g : X ⟶ Spec (CommRingCat.of A))
    [QuasiCompact g] [QuasiSeparated g] [LocallyOfFinitePresentation g]
    (U V : X.Opens) (hUV : U ⊔ V = ⊤) (hUc : IsCompact (U : Set ↥X)) (hVc : IsCompact (V : Set ↥X))
    (hU : ∀ SS : Finset A, ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑SS : Set A) ⊆ T ∧ Set.range
      (algebraMap R A) ⊆ T ∧
        ∃ (X₀ : Scheme.{u}) (f₀ : X₀ ⟶ Spec (CommRingCat.of ↥T)) (π : (U : Scheme.{u}) ⟶ X₀),
          LocallyOfFinitePresentation f₀ ∧ QuasiCompact f₀ ∧ QuasiSeparated f₀ ∧
          IsPullback π (U.ι ≫ g) f₀ (Spec.map (CommRingCat.ofHom (algebraMap ↥T A))))
    (hV : ∀ SS : Finset A, ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑SS : Set A) ⊆ T ∧ Set.range
      (algebraMap R A) ⊆ T ∧
        ∃ (X₀ : Scheme.{u}) (f₀ : X₀ ⟶ Spec (CommRingCat.of ↥T)) (π : (V : Scheme.{u}) ⟶ X₀),
          LocallyOfFinitePresentation f₀ ∧ QuasiCompact f₀ ∧ QuasiSeparated f₀ ∧
          IsPullback π (V.ι ≫ g) f₀ (Spec.map (CommRingCat.ofHom (algebraMap ↥T A))))
    (SS : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑SS : Set A) ⊆ T ∧ Set.range (algebraMap R A) ⊆ T ∧
        ∃ (X₀ : Scheme.{u}) (f₀ : X₀ ⟶ Spec (CommRingCat.of ↥T)) (π : X ⟶ X₀),
          LocallyOfFinitePresentation f₀ ∧ QuasiCompact f₀ ∧ QuasiSeparated f₀ ∧
          IsPullback π g f₀ (Spec.map (CommRingCat.ofHom (algebraMap ↥T A)))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.