Module

ConstantPresentation.lean

Nyll.EtaleCohomology.Sites.ConstantPresentation

5 declarations indexed from sourceView source ↗

Module documentation

Local factorization of finitely generated constant modules

A map from a constant presheaf of finitely generated modules locally factors through any locally bijective constant presentation of its target. A finite intersection of covering image sieves puts all generators in the image. On a neighborhood containing a chosen point, local injectivity of the constant presentation is genuine injectivity, so the resulting lift is linear.

Imports11

Nyll.EtaleCohomology.Sites.ConstantRepresentable
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.AlgebraicGeometry.Sites.Small
Mathlib.Algebra.Module.Submodule.Equiv
Mathlib.Algebra.Module.Submodule.Range
Mathlib.CategoryTheory.Sites.LocallyInjective
Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.RingTheory.Finiteness.Defs
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.Algebra.Category.ModuleCat.Basic

Imported by7

lemma

exists_etale_neighborhood_in_sieve

L36 ↗

EtaleCohomology.exists_etale_neighborhood_in_sieve

Documentation

Every point has a neighborhood belonging to a covering sieve of the small étale site.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology

Lean source · statement

lemma exists_etale_neighborhood_in_sieve {X : Scheme.{u}} {W : X.Etale}
    (S : Sieve W) (hS : S ∈ X.smallEtaleTopology W) (x : W.left) :
    ∃ (Y : X.Etale) (g : Y ⟶ W) (y : Y.left), S g ∧ g.left y = x

lemma

finset_inf_cover

L48 ↗

EtaleCohomology.finset_inf_cover

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology

Lean source · statement

lemma finset_inf_cover {C : Type*} [Category* C]
    (J : GrothendieckTopology C) {W : C} {ι : Type*}
    (s : Finset ι) (S : ι → Sieve W) (hS : ∀ i ∈ s, S i ∈ J W) :
    s.inf S ∈ J W

lemma

constantPresentation_app_injective

L65 ↗

EtaleCohomology.constantPresentation_app_injective

Documentation

A locally injective constant presentation is injective on every nonempty étale object.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

lemma constantPresentation_app_injective
    {M : ModuleCat.{u} R} {F : X.Etaleᵒᵖ ⥤ ModuleCat.{u} R}
    (η : (Functor.const X.Etaleᵒᵖ).obj M ⟶ F)
    [Presheaf.IsLocallyInjective X.smallEtaleTopology η]
    (W : X.Etale) (x : W.left) : Function.Injective (η.app (op W))

theorem

exists_constantPresentation_factor

L78 ↗

EtaleCohomology.exists_constantPresentation_factor

Documentation

Finitely many generators can be lifted on one actual étale neighborhood, and local injectivity makes the lift a module homomorphism.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem exists_constantPresentation_factor
    (M N : ModuleCat.{u} R) [Module.Finite R M]
    {F : X.Etaleᵒᵖ ⥤ ModuleCat.{u} R}
    (α : (Functor.const X.Etaleᵒᵖ).obj M ⟶ F)
    (η : (Functor.const X.Etaleᵒᵖ).obj N ⟶ F)
    [Presheaf.IsLocallyInjective X.smallEtaleTopology η]
    [Presheaf.IsLocallySurjective X.smallEtaleTopology η]
    (x : X) : ∃ (Y : X.Etale) (y : Y.left) (l : M ⟶ N),
      Y.hom y = x ∧ α.app (op Y) = l ≫ η.app (op Y)

theorem

exists_constantFreePresentation_lift

L123 ↗

EtaleCohomology.exists_constantFreePresentation_lift

Documentation

A map from a finite free constant presheaf locally lifts through a locally surjective morphism, by lifting the finitely many basis vectors simultaneously.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem exists_constantFreePresentation_lift (n : ℕ)
    {G H : X.Etaleᵒᵖ ⥤ ModuleCat.{u} R}
    (α : (Functor.const X.Etaleᵒᵖ).obj (ModuleCat.of R (Fin n →₀ R)) ⟶ H)
    (η : G ⟶ H) [Presheaf.IsLocallySurjective X.smallEtaleTopology η]
    (x : X) : ∃ (Y : X.Etale) (y : Y.left)
      (l : ModuleCat.of R (Fin n →₀ R) ⟶ G.obj (op Y)),
      Y.hom y = x ∧ l ≫ η.app (op Y) = α.app (op Y)

Module documentation

Local factorization of finitely generated constant modules

Declarations

exists_etale_neighborhood_in_sieve

finset_inf_cover

constantPresentation_app_injective

exists_constantPresentation_factor

exists_constantFreePresentation_lift