NYLL
Module

LocallyConstantProducts.lean

Nyll.EtaleCohomology.Constructible.LocallyConstantProducts
2 declarations indexed from sourceView source ↗

Module documentation

Products of locally constant module sheaves

Refining the two trivializing étale covers gives constant models for a binary product. Both inverse image and the constant-sheaf functor preserve binary products, and a product of finitely generated modules is finitely generated.

Imports16
Imported by4

Declarations

theorem

prod

L41 ↗
EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.prod
Documentation

Binary products preserve finite type local constancy over any coefficient ring.

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 IsEtaleFiniteTypeLocallyConstant.prod
    {X : Scheme.{u}} {R : Type u} [CommRing R]
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleFiniteTypeLocallyConstant R G)
    (hH : IsEtaleFiniteTypeLocallyConstant R H) :
    IsEtaleFiniteTypeLocallyConstant R (G ⨯ H)
theorem

selfProd

L77 ↗
EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.selfProd
Documentation

In particular, the square used to express addition is finite type locally constant.

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 IsEtaleFiniteTypeLocallyConstant.selfProd
    {X : Scheme.{u}} {R : Type u} [CommRing R]
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleFiniteTypeLocallyConstant R G) :
    IsEtaleFiniteTypeLocallyConstant R (G ⨯ G)

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