NYLL
Module

IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
14 declarations indexed from sourceView source ↗

Module documentation

Is Separated exists fg subalgebra of is Separated pullback snd

Imports1
Imported by3

Declarations

def

eT

L56 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.eT
Documentation

The comparison isomorphism between the target pullbacks of the base-changed chart.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section bridge
variable {U U' X S Y : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S) (g : Y ⟶ S)
Lean source · full declaration
def eT :
    pullback (pullback.snd a (pullback.fst f g) ≫ pullback.snd f g) (pullback.snd b (pullback.fst f
      g) ≫ pullback.snd f g) ≅ pullback (pullback.fst (a ≫ f) (b ≫ f) ≫ a ≫ f) g where
  hom := pullback.lift
    (pullback.lift (pullback.fst _ _ ≫ pullback.fst a (pullback.fst f g)) (pullback.snd _ _ ≫
      pullback.fst b (pullback.fst f g))
      (by
        have hT := pullback.condition_assoc (f := pullback.snd a (pullback.fst f g) ≫ pullback.snd
          f g) (g := pullback.snd b (pullback.fst f g) ≫ pullback.snd f g) g
        simp only [Category.assoc] at hT
        simp only [Category.assoc]
        rw [pullback.condition_assoc (f := a) (g := pullback.fst f g), pullback.condition (f := f)
          (g := g), hT,
          ← pullback.condition (f := f) (g := g), ← pullback.condition_assoc (f := b) (g :=
            pullback.fst f g)]))
    (pullback.fst _ _ ≫ pullback.snd a (pullback.fst f g) ≫ pullback.snd f g)
    (by
      simp only [Category.assoc, pullback.lift_fst_assoc]
      rw [pullback.condition_assoc (f := a) (g := pullback.fst f g), pullback.condition (f := f) (g
        := g)])
  inv := pullback.lift
    (pullback.lift (pullback.fst _ _ ≫ pullback.fst (a ≫ f) (b ≫ f))
      (pullback.lift (pullback.fst _ _ ≫ pullback.fst (a ≫ f) (b ≫ f) ≫ a) (pullback.snd _ _)
        (by simpa only [Category.assoc] using
          pullback.condition (f := (pullback.fst (a ≫ f) (b ≫ f) ≫ a ≫ f)) (g := g)))
      (by simp))
    (pullback.lift (pullback.fst _ _ ≫ pullback.snd (a ≫ f) (b ≫ f))
      (pullback.lift (pullback.fst _ _ ≫ pullback.snd (a ≫ f) (b ≫ f) ≫ b) (pullback.snd _ _)
        (by
          simp only [Category.assoc]
          rw [← pullback.condition (f := a ≫ f) (g := b ≫ f)]
          simpa only [Category.assoc] using pullback.condition (f := (pullback.fst (a ≫ f) (b ≫ f)
            ≫ a ≫ f)) (g := g)))
      (by simp))
    (by simp)
  hom_inv_id := by
    ext <;> simp [pullback.condition]
  inv_hom_id := by
    ext <;> simp
def

eS

L97 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.eS
Documentation

The comparison isomorphism between the source pullbacks of the base-changed chart.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section bridge
variable {U U' X S Y : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S) (g : Y ⟶ S)
Lean source · full declaration
def eS :
    pullback (pullback.snd a (pullback.fst f g)) (pullback.snd b (pullback.fst f g)) ≅ pullback
      (pullback.mapDesc a b f ≫ pullback.fst (a ≫ f) (b ≫ f) ≫ a ≫ f) g where
  hom := pullback.lift
    (pullback.lift (pullback.fst _ _ ≫ pullback.fst a (pullback.fst f g)) (pullback.snd _ _ ≫
      pullback.fst b (pullback.fst f g))
      (by
        have hS := pullback.condition_assoc (f := pullback.snd a (pullback.fst f g)) (g :=
          pullback.snd b (pullback.fst f g)) (pullback.fst f g)
        simp only [Category.assoc]
        rw [pullback.condition (f := a) (g := pullback.fst f g), hS, ← pullback.condition (f := b)
          (g := pullback.fst f g)]))
    (pullback.fst _ _ ≫ pullback.snd a (pullback.fst f g) ≫ pullback.snd f g)
    (by
      simp only [Category.assoc, pullback.lift_fst_assoc, Category.comp_id]
      rw [pullback.condition_assoc (f := a) (g := pullback.fst f g), pullback.condition (f := f) (g
        := g)])
  inv := pullback.lift
    (pullback.lift (pullback.fst _ _ ≫ pullback.fst a b)
      (pullback.lift (pullback.fst _ _ ≫ pullback.fst a b ≫ a) (pullback.snd _ _)
        (by
          have := pullback.condition (f := (pullback.mapDesc a b f ≫ pullback.fst (a ≫ f) (b ≫ f) ≫
            a ≫ f)) (g := g)
          simp only [pullback.lift_fst_assoc, Category.comp_id] at this
          simpa only [Category.assoc] using this))
      (by simp))
    (pullback.lift (pullback.fst _ _ ≫ pullback.snd a b)
      (pullback.lift (pullback.fst _ _ ≫ pullback.fst a b ≫ a) (pullback.snd _ _)
        (by
          have := pullback.condition (f := (pullback.mapDesc a b f ≫ pullback.fst (a ≫ f) (b ≫ f) ≫
            a ≫ f)) (g := g)
          simp only [pullback.lift_fst_assoc, Category.comp_id] at this
          simpa only [Category.assoc] using this))
      (by simp [pullback.condition]))
    (by simp)
  hom_inv_id := by
    have hS2 := pullback.condition_assoc (f := pullback.snd a (pullback.fst f g)) (g :=
      pullback.snd b (pullback.fst f g)) (pullback.snd f g)
    ext <;> simp [pullback.condition, hS2]
  inv_hom_id := by
    ext <;> simp
lemma

eS_hom_mY

L139 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.eS_hom_mY
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section bridge
variable {U U' X S Y : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S) (g : Y ⟶ S)
Lean source · full declaration
lemma eS_hom_mY :
    (eS a b f g).hom ≫ pullback.map (pullback.mapDesc a b f ≫ pullback.fst (a ≫ f) (b ≫ f) ≫ a ≫ f)
      g (pullback.fst (a ≫ f) (b ≫ f) ≫ a ≫ f) g (pullback.mapDesc a b f) (𝟙 Y) (𝟙 S)
      (by simp) (by simp) =
      pullback.mapDesc (pullback.snd a (pullback.fst f g)) (pullback.snd b (pullback.fst f g))
        (pullback.snd f g) ≫ (eT a b f g).hom := by
  have hS2 := pullback.condition_assoc (f := pullback.snd a (pullback.fst f g)) (g := pullback.snd
    b (pullback.fst f g)) (pullback.snd f g)
  ext <;> simp [eS, eT, pullback.condition, hS2]
theorem

isClosedImmersion_iff

L149 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.isClosedImmersion_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section bridge
variable {U U' X S Y : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S) (g : Y ⟶ S)
Lean source · full declaration
theorem isClosedImmersion_iff :
    IsClosedImmersion (pullback.mapDesc (pullback.snd a (pullback.fst f g)) (pullback.snd b
      (pullback.fst f g)) (pullback.snd f g)) ↔
      IsClosedImmersion (pullback.map (pullback.mapDesc a b f ≫ pullback.fst (a ≫ f) (b ≫ f) ≫ a ≫
        f) g (pullback.fst (a ≫ f) (b ≫ f) ≫ a ≫ f) g (pullback.mapDesc a b f) (𝟙 Y) (𝟙 S)
        (by simp) (by simp)) := by
  rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion
    (pullback.mapDesc (pullback.snd a (pullback.fst f g)) (pullback.snd b (pullback.fst f g))
      (pullback.snd f g)) (eT a b f g).hom, ← eS_hom_mY,
    MorphismProperty.cancel_left_of_respectsIso @IsClosedImmersion (eS a b f g).hom]
abbrev

chart

L167 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.chart
Documentation

The map between pairwise chart intersections induced by the structure morphism.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · statement
abbrev chart
abbrev

chartBase

L170 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.chartBase
Documentation

The structure map of the pairwise chart pullback to the base scheme.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · statement
abbrev chartBase : pullback (a ≫ f) (b ≫ f) ⟶ S
abbrev

chartBC

L174 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.chartBC
Documentation

The base change of the pairwise chart comparison map.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · statement
abbrev chartBC {Y : Scheme.{u}} (g : Y ⟶ S) :
    pullback (chart a b f ≫ chartBase a b f) g ⟶ pullback (chartBase a b f) g
lemma

chartBC_fst

L179 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.chartBC_fst
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · statement
lemma chartBC_fst {Y : Scheme.{u}} (g : Y ⟶ S) :
    chartBC a b f g ≫ pullback.fst _ _ = pullback.fst _ _ ≫ chart a b f
lemma

chartBC_snd

L182 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.chartBC_snd
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · statement
lemma chartBC_snd {Y : Scheme.{u}} (g : Y ⟶ S) :
    chartBC a b f g ≫ pullback.snd _ _ = pullback.snd _ _
lemma

eq_chartBC

L185 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.eq_chartBC
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · statement
lemma eq_chartBC {Y : Scheme.{u}} (g : Y ⟶ S)
    (m' : pullback (chart a b f ≫ chartBase a b f) g ⟶ pullback (chartBase a b f) g)
    (h₁ : m' ≫ pullback.fst _ _ = pullback.fst _ _ ≫ chart a b f) (h₂ : m' ≫ pullback.snd _ _ =
      pullback.snd _ _) :
    m' = chartBC a b f g
lemma

isPullback_stage

L194 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.isPullback_stage
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · full declaration
lemma isPullback_stage {Z Y₁ Y₂ : Scheme.{u}} (h : Z ⟶ S) (g₁ : Y₁ ⟶ S) (g₂ : Y₂ ⟶ S) (κ : Y₂ ⟶ Y₁)
    (hκ : κ ≫ g₁ = g₂) :
    IsPullback (pullback.snd h g₂) (pullback.map h g₂ h g₁ (𝟙 Z) κ (𝟙 S) (by simp) (by simp [hκ])) κ
      (pullback.snd h g₁) := by
  apply IsPullback.flip
  refine IsPullback.of_right (h₁₂ := pullback.fst h g₁) (v₁₃ := h) (h₂₂ := g₁) ?_ (by simp)
    (IsPullback.of_hasPullback h g₁)
  simp only [pullback.lift_fst, Category.comp_id, hκ]
  exact IsPullback.of_hasPullback h g₂
lemma

isClosedImmersion_chartBC_of_fac

L204 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.isClosedImmersion_chartBC_of_fac
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section charts
variable {U U' X S : Scheme.{u}} (a : U ⟶ X) (b : U' ⟶ X) (f : X ⟶ S)
Lean source · statement
lemma isClosedImmersion_chartBC_of_fac {Y₁ Y₂ : Scheme.{u}} (g₁ : Y₁ ⟶ S) (g₂ : Y₂ ⟶ S) (κ : Y₂ ⟶
  Y₁)
    (hκ : κ ≫ g₁ = g₂) (H : IsClosedImmersion (chartBC a b f g₁)) : IsClosedImmersion (chartBC a b
      f g₂)
theorem

isSeparated_snd_iff

L226 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd.SepDescAux.isSeparated_snd_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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 SepDescAux
section key
variable {X S : Scheme.{u}} (f : X ⟶ S) (𝒰 : X.OpenCover) [∀ i, IsAffine (𝒰.X i)] [IsAffine S]
  {Y : Scheme.{u}} [IsAffine Y] (g : Y ⟶ S)
include 𝒰 in
Lean source · statement
theorem isSeparated_snd_iff :
    IsSeparated (pullback.snd f g) ↔ ∀ i j : 𝒰.I₀, IsClosedImmersion (chartBC (𝒰.f i) (𝒰.f j) f g)
theorem

exists_fg_subalgebra_of_isSeparated_pullback_snd

L266 ↗
AlgebraicGeometry.IsSeparated.exists_fg_subalgebra_of_isSeparated_pullback_snd
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsSeparated_exists_fg_subalgebra_of_isSeparated_pullback_snd
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
open SepDescAux in
Lean source · statement
theorem _root_.AlgebraicGeometry.IsSeparated.exists_fg_subalgebra_of_isSeparated_pullback_snd
    {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A₀)) [QuasiCompact f] [QuasiSeparated f]
    [IsSeparated (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))))] (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
      IsSeparated (pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))))

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