Module

FiniteSurjectiveUnit.lean

Nyll.EtaleCohomology.Sites.FiniteSurjectiveUnit

1 declaration indexed from sourceView source ↗

Module documentation

Injectivity of the actual unit for a finite surjection

Choose algebraically closed residue-field points on the target. Surjectivity and finiteness supply a lift of each of these points using the same field. The unit followed by its concrete stalk component is an isomorphism, so the unit is injective on every stalk of this conservative family.

Imports10

Nyll.EtaleCohomology.Sites.PullbackUnitGeometricStalks
Nyll.EtaleCohomology.Sites.PushforwardStalkComparison
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.SchemeTheory.Etale.FiniteGeometricPoints
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Sites.Point.Conservative
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Imported by2

theorem

etaleFiniteSurjective_unit_mono

L38 ↗

EtaleCohomology.etaleFiniteSurjective_unit_mono

Documentation

The inverse-image/direct-image unit for a finite surjection is a monomorphism for every étale module sheaf.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology

Lean source · statement

theorem etaleFiniteSurjective_unit_mono
    {X Y : Scheme.{u}} (q : Y ⟶ X) [IsFinite q] [Surjective q]
    (Λ : Type u) [CommRing Λ]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    Mono ((etalePullbackPushforwardAdjunction q Λ).unit.app F)

Module documentation

Injectivity of the actual unit for a finite surjection

Declarations

etaleFiniteSurjective_unit_mono