Module

OpenImmersionUnit.lean

Nyll.SchemeTheory.Modules.OpenImmersionUnit

1 declaration indexed from sourceView source ↗

Module documentation

Pullback-pushforward units on the image of an open immersion

The unit is bijective on sections over opens contained in the image of the immersion.

Imports1

Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by13

theorem

bijective_unit_app_of_le_opensRange

L29 ↗

AlgebraicGeometry.Scheme.Modules.bijective_unit_app_of_le_opensRange

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_bijective_unit_app_of_le_opensRange
universe u
open CategoryTheory AlgebraicGeometry Opposite AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.bijective_unit_app_of_le_opensRange
    {X Y : Scheme.{u}} (j : Y ⟶ X) [IsOpenImmersion j] (N : X.Modules)
    (V : X.Opens) (hV : V ≤ j.opensRange) :
    Function.Bijective (((Scheme.Modules.pullbackPushforwardAdjunction j).unit.app N).app V)

Module documentation

Pullback-pushforward units on the image of an open immersion

Declarations

bijective_unit_app_of_le_opensRange