NYLL
Module

IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact.lean

Nyll.AlgebraicCurves.Geometry.Schemes.IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact
4 declarations indexed from sourceView source ↗

Module documentation

Is Closed Immersion exists fg subalgebra of is Closed Immersion pullback map of quasi

Compact

Imports2
Imported by2

Declarations

theorem

isPullback_fst_of_comm

L55 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact.ClosedImmQc18.isPullback_fst_of_comm
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact
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 v
namespace ClosedImmQc18
variable {W V V' S B : Scheme.{u}} (m : W ⟶ V) (v : V ⟶ S) (ι : V' ⟶ V) (b : B ⟶ S)
Lean source · statement
theorem isPullback_fst_of_comm
    (μ : pullback (m ≫ v) b ⟶ pullback v b) (hμ₁ : μ ≫ pullback.fst v b = pullback.fst (m ≫ v) b ≫
      m)
    (hμ₂ : μ ≫ pullback.snd v b = pullback.snd (m ≫ v) b) :
    IsPullback μ (pullback.fst (m ≫ v) b) (pullback.fst v b) m
theorem

isPullback_chart

L64 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact.ClosedImmQc18.isPullback_chart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact
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 v
namespace ClosedImmQc18
variable {W V V' S B : Scheme.{u}} (m : W ⟶ V) (v : V ⟶ S) (ι : V' ⟶ V) (b : B ⟶ S)
Lean source · statement
theorem isPullback_chart
    (μ : pullback (m ≫ v) b ⟶ pullback v b) (hμ₁ : μ ≫ pullback.fst v b = pullback.fst (m ≫ v) b ≫
      m)
    (hμ₂ : μ ≫ pullback.snd v b = pullback.snd (m ≫ v) b)
    (μ' : pullback (pullback.snd m ι ≫ ι ≫ v) b ⟶ pullback (ι ≫ v) b)
    (hμ'₁ : μ' ≫ pullback.fst (ι ≫ v) b = pullback.fst _ b ≫ pullback.snd m ι)
    (hμ'₂ : μ' ≫ pullback.snd (ι ≫ v) b = pullback.snd _ b)
    (κ : pullback (ι ≫ v) b ⟶ pullback v b) (hκ₁ : κ ≫ pullback.fst v b = pullback.fst (ι ≫ v) b ≫
      ι)
    (hκ₂ : κ ≫ pullback.snd v b = pullback.snd (ι ≫ v) b)
    (lam : pullback (pullback.snd m ι ≫ ι ≫ v) b ⟶ pullback (m ≫ v) b)
    (hlam₁ : lam ≫ pullback.fst (m ≫ v) b = pullback.fst _ b ≫ pullback.fst m ι)
    (hlam₂ : lam ≫ pullback.snd (m ≫ v) b = pullback.snd _ b) :
    IsPullback lam μ' μ κ
theorem

fg_finset_sup

L103 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact.ClosedImmQc18.fg_finset_sup
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact
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 v
namespace ClosedImmQc18
Lean source · statement
theorem fg_finset_sup {R L : Type u} [CommRing R] [CommRing L] [Algebra R L] {ι' : Type v} (G :
  Finset ι')
    (T : ι' → Subalgebra R L) (h : ∀ i ∈ G, (T i).FG) : (G.sup T).FG
theorem

exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact

L127 ↗
AlgebraicGeometry.IsClosedImmersion.exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry.IsClosedImmersion
universe u v
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open IsClosedImmersion_exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in
open ClosedImmQc18 in
Lean source · statement
theorem exists_fg_subalgebra_of_isClosedImmersion_pullback_map_of_quasiCompact
    {A₀ : Type u} [CommRing A₀] {A : Type u} [CommRing A] [Algebra A₀ A]
    {W V : Scheme.{u}} (m : W ⟶ V) (v : V ⟶ Spec (CommRingCat.of A₀)) [QuasiCompact v]
    [QuasiCompact m] [QuasiSeparated m] [LocallyOfFiniteType m]
    (hA : ∀ mA : pullback (m ≫ v) (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))) ⟶
        pullback v (Spec.map (CommRingCat.ofHom (algebraMap A₀ A))),
      mA ≫ pullback.fst _ _ = pullback.fst _ _ ≫ m → mA ≫ pullback.snd _ _ = pullback.snd _ _ →
      IsClosedImmersion mA)
    (s : Finset A) :
    ∃ (T : Subalgebra A₀ A), T.FG ∧ (↑s : Set A) ⊆ T ∧
      ∀ mT : pullback (m ≫ v) (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))) ⟶
          pullback v (Spec.map (CommRingCat.ofHom (algebraMap A₀ ↥T))),
        mT ≫ pullback.fst _ _ = pullback.fst _ _ ≫ m → mT ≫ pullback.snd _ _ = pullback.snd _ _ →
        IsClosedImmersion mT

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