NYLL
Module

InverseLimitOpenEquations.lean

Nyll.SchemeTheory.FiniteEtale.InverseLimitOpenEquations
7 declarations indexed from sourceView source ↗

Module documentation

Simultaneous equations over inverse-limit overlaps

Compact stage opens, including pairwise and triple intersections of affine charts in a quasi-separated scheme, give actual quasi-compact restricted inverse systems. A finite family of equations over different such opens holds at one common original stage. Finiteness is required only over each open, not over the ambient scheme.

Imports4
Imported by2

Declarations

theorem

opensDiagram_obj_compactSpace

L32 ↗
AlgebraicGeometry.opensDiagram_obj_compactSpace
Documentation

Quasi-compactness of an open propagates to every stage of its actual restricted inverse system under affine transition maps.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
Lean source · statement
theorem opensDiagram_obj_compactSpace
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u})
    [∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h)]
    (i : I) (U : (D.obj i).Opens) (hU : IsCompact (U : Set (D.obj i)))
    (j : Over i) : CompactSpace ((opensDiagram D i U).obj j)
theorem

opensDiagram_obj_quasiSeparatedSpace

L42 ↗
AlgebraicGeometry.opensDiagram_obj_quasiSeparatedSpace
Documentation

The opens in the restricted inverse system inherit quasi-separatedness from their actual ambient stages.

Source context 4 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
Lean source · statement
theorem opensDiagram_obj_quasiSeparatedSpace
    {I : Type u} [Category.{u} I] (D : I ⥤ Scheme.{u})
    [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) (U : (D.obj i).Opens) (j : Over i) :
    QuasiSeparatedSpace ((opensDiagram D i U).obj j)
instance

finiteEtaleOverCategoryOpenEquations

L52 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryOpenEquations
Source context 5 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
namespace FiniteEtale
Lean source · statement
instance finiteEtaleOverCategoryOpenEquations (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X)
instance

finiteEtaleHasPullbacksAlongOpenEquations

L56 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongOpenEquations
Source context 6 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
namespace FiniteEtale
local instance finiteEtaleOverCategoryOpenEquations (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
Lean source · statement
instance finiteEtaleHasPullbacksAlongOpenEquations
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
instance

finiteEtaleStableUnderBaseChangeAlongOpenEquations

L62 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongOpenEquations
Source context 7 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
namespace FiniteEtale
local instance finiteEtaleOverCategoryOpenEquations (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOpenEquations
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
Lean source · statement
instance finiteEtaleStableUnderBaseChangeAlongOpenEquations
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f
theorem

map_eq_of_comparison

L69 ↗
AlgebraicGeometry.FiniteEtale.map_eq_of_comparison
Source context 8 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
namespace FiniteEtale
local instance finiteEtaleOverCategoryOpenEquations (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOpenEquations
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongOpenEquations
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
Lean source · statement
theorem map_eq_of_comparison
    {C₀ C₁ : Type*} [Category* C₀] [Category* C₁]
    {F G : C₀ ⥤ C₁} (e : F ≅ G) {A B : C₀} (a b : A ⟶ B)
    (h : G.map a = G.map b) : F.map a = F.map b
theorem

exists_inverse_limit_open_stage_map_eq_family

L79 ↗
AlgebraicGeometry.FiniteEtale.exists_inverse_limit_open_stage_map_eq_family
Documentation

A finite family of native equations over possibly different compact stage opens descends simultaneously. The sources and targets need only be finite etale over their respective opens.

Source context 8 commands

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

noncomputable section
universe u v
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry
namespace FiniteEtale
local instance finiteEtaleOverCategoryOpenEquations (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongOpenEquations
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongOpenEquations
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.IsStableUnderBaseChangeAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun h hf ↦ MorphismProperty.of_isPullback
    (P := (@IsFiniteEtale : MorphismProperty Scheme.{u})) h hf⟩
Lean source · statement
theorem exists_inverse_limit_open_stage_map_eq_family
    {I : Type u} [Category.{u} I] [IsCofiltered I]
    (D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
    [∀ {i j : I} (h : i ⟶ j), IsAffineHom (D.map h)]
    (i : I) {K : Type v} [Finite K]
    (U : K → (D.obj i).Opens)
    (hU : ∀ k : K, IsCompact (U k : Set (D.obj i)))
    (t : Over i)
    (A B : ∀ k : K, FiniteEtale ((opensDiagram D i (U k)).obj t))
    (a b : ∀ k : K, A k ⟶ B k)
    (hab : ∀ k : K,
      (FiniteEtale.pullback ((opensCone D c i (U k)).π.app t)).map (a k) =
        (FiniteEtale.pullback ((opensCone D c i (U k)).π.app t)).map (b k)) :
    ∃ (s : Over i) (hst : s ⟶ t), ∀ k : K,
      (FiniteEtale.pullback ((opensDiagram D i (U k)).map hst)).map (a k) =
        (FiniteEtale.pullback ((opensDiagram D i (U k)).map hst)).map (b k)

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