Module

Scheme_IdealSheafData_range_moduleIota_app_and_injective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_range_moduleIota_app_and_injective

1 declaration indexed from sourceView source ↗

Module documentation

The range of an ideal-module inclusion

On an affine open, the module inclusion is injective and its range is the corresponding ideal of ring sections.

Imports1

Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModule

Imported by10

theorem

range_moduleIota_app_and_injective

L31 ↗

AlgebraicGeometry.Scheme.IdealSheafData.range_moduleIota_app_and_injective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_range_moduleIota_app_and_injective
universe u
open CategoryTheory CategoryTheory.Limits
open AlgebraicGeometry Opposite in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.range_moduleIota_app_and_injective {X :
  Scheme.{u}} (I : X.IdealSheafData) (U : X.affineOpens) :
    Set.range (I.moduleι.app U) = (I.ideal U : Set Γ(X, U)) ∧
      Function.Injective (I.moduleι.app U)

Module documentation

The range of an ideal-module inclusion

Declarations

range_moduleIota_app_and_injective