Module

SectionImageGluing.lean

Nyll.EtaleCohomology.Sites.SectionImageGluing

1 declaration indexed from sourceView source ↗

Module documentation

Gluing a section in the local image of an injective sheaf morphism

This is the single-section version of the gluing argument in CategoryTheory.Sheaf.isLocallyBijective_iff_isIso', from Mathlib/CategoryTheory/Sites/LocallyBijective.lean by Joël Riou. Only the image sieve of the specified section needs to cover.

Imports2

Mathlib.CategoryTheory.Sites.LocallySurjective
Mathlib.CategoryTheory.Sites.Sheaf

Imported by2

theorem

exists_section_lift_of_imageSieve_mem

L30 ↗

EtaleCohomology.Sites.exists_section_lift_of_imageSieve_mem

Documentation

A section locally in the image of an objectwise injective sheaf morphism has a global preimage.

Source context 4 commands

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

noncomputable section
open CategoryTheory Opposite
namespace EtaleCohomology.Sites
universe u v w

Lean source · statement

theorem exists_section_lift_of_imageSieve_mem
    {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
    {F G : Sheaf J (Type w)} (η : F ⟶ G)
    (hη : ∀ U : Cᵒᵖ, Function.Injective (η.hom.app U))
    {U : C} (s : G.obj.obj (op U))
    (hs : Presheaf.imageSieve η.hom s ∈ J U) :
    ∃ a : F.obj.obj (op U), η.hom.app (op U) a = s

Module documentation

Gluing a section in the local image of an injective sheaf morphism

Declarations

exists_section_lift_of_imageSieve_mem