NYLL
Module

InverseLimitIsomorphism.lean

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

Module documentation

Isomorphisms and finite equation families at inverse-system stages

Native Hom descent supplies an inverse map, and native eventual equality makes both inverse equations hold at a common actual stage. No projection is assumed faithfully flat, surjective, or faithful on finite-etale covers.

Imports4
Imported by2

Declarations

instance

finiteEtaleOverCategoryLimitIso

L28 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleOverCategoryLimitIso
Source context 4 commands

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

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

finiteEtaleHasPullbacksAlongLimitIso

L32 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleHasPullbacksAlongLimitIso
Source context 5 commands

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

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

finiteEtaleStableUnderBaseChangeAlongLimitIso

L38 ↗
AlgebraicGeometry.FiniteEtale.finiteEtaleStableUnderBaseChangeAlongLimitIso
Source context 6 commands

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

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

map_eq_of_comparison

L45 ↗
AlgebraicGeometry.FiniteEtale.map_eq_of_comparison
Source context 7 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongLimitIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitIso
    {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

inverse_equations_of_comparison

L52 ↗
AlgebraicGeometry.FiniteEtale.inverse_equations_of_comparison
Source context 7 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongLimitIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitIso
    {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 inverse_equations_of_comparison
    {C₀ C₁ C₂ : Type*} [Category* C₀] [Category* C₁] [Category* C₂]
    (F : C₀ ⥤ C₂) (U : C₀ ⥤ C₁) (V : C₁ ⥤ C₂) (e : F ≅ U ⋙ V)
    {A B : C₀} (a : A ⟶ B) [IsIso (F.map a)] (b : U.obj B ⟶ U.obj A)
    (hb : e.hom.app B ≫ V.map b = inv (F.map a) ≫ e.hom.app A) :
    V.map (U.map a ≫ b) = 𝟙 (V.obj (U.obj A)) ∧
      V.map (b ≫ U.map a) = 𝟙 (V.obj (U.obj B))
theorem

exists_inverse_limit_stage_map_eq_family

L81 ↗
AlgebraicGeometry.FiniteEtale.exists_inverse_limit_stage_map_eq_family
Documentation

A finite collection of equalities of native finite-etale morphisms holds after one common transition if it holds over the actual limit.

Source context 9 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongLimitIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitIso
    {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⟩
variable {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, CompactSpace (D.obj i)]
include hc
Lean source · statement
theorem exists_inverse_limit_stage_map_eq_family
    (i : I) {K : Type v} [Finite K] (A B : K → FiniteEtale (D.obj i))
    (a b : ∀ k : K, A k ⟶ B k)
    (hab : ∀ k : K, (FiniteEtale.pullback (c.π.app i)).map (a k) =
      (FiniteEtale.pullback (c.π.app i)).map (b k)) :
    ∃ (j : I) (hji : j ⟶ i), ∀ k : K,
      (FiniteEtale.pullback (D.map hji)).map (a k) =
        (FiniteEtale.pullback (D.map hji)).map (b k)
theorem

exists_inverse_limit_stage_isIso

L107 ↗
AlgebraicGeometry.FiniteEtale.exists_inverse_limit_stage_isIso
Documentation

A morphism of finite-etale models which becomes an isomorphism over the limit is an isomorphism after an actual later transition. The inverse and both inverse equations are constructed by descent.

Source context 9 commands

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

noncomputable section
universe u v
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleOverCategoryLimitIso (X : Scheme.{u}) :
    Category (MorphismProperty.Over
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) ⊤ X) := instCategory X
local instance finiteEtaleHasPullbacksAlongLimitIso
    {X Y : Scheme.{u}} (f : X ⟶ Y) :
    MorphismProperty.HasPullbacksAlong
      (@IsFiniteEtale : MorphismProperty Scheme.{u}) f :=
  ⟨fun _ _ ↦ inferInstance⟩
local instance finiteEtaleStableUnderBaseChangeAlongLimitIso
    {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⟩
variable {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, CompactSpace (D.obj i)]
include hc
Lean source · statement
theorem exists_inverse_limit_stage_isIso
    [∀ i : I, QuasiSeparatedSpace (D.obj i)]
    (i : I) {A B : FiniteEtale (D.obj i)} (a : A ⟶ B)
    [IsIso ((FiniteEtale.pullback (c.π.app i)).map a)] :
    ∃ (j : I) (hji : j ⟶ i), IsIso ((FiniteEtale.pullback (D.map hji)).map a)

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