Module

Scheme_IdealSheafData_eq_of_forall_comap_openCover_eq.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_eq_of_forall_comap_openCover_eq

2 declarations indexed from sourceView source ↗

Module documentation

Equality of ideal sheaves on an open cover

Ideal-sheaf data agree when their pullbacks to every member of an open cover agree.

Imports2

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.Cover.Open

Imported by4

theorem

eq_of_forall_comap_openCover_eq_aux

L43 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_eq_of_forall_comap_openCover_eq.AlgebraicGeometry.Scheme.IdealSheafData.eq_of_forall_comap_openCover_eq_aux

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_eq_of_forall_comap_openCover_eq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry

Lean source · statement

theorem eq_of_forall_comap_openCover_eq_aux
    {X : Scheme.{u}} (𝒰 : X.OpenCover) {I J : X.IdealSheafData}
    (h : ∀ i, I.comap (𝒰.f i) = J.comap (𝒰.f i)) : I = J

theorem

eq_of_forall_comap_openCover_eq

L62 ↗

AlgebraicGeometry.Scheme.IdealSheafData.eq_of_forall_comap_openCover_eq

Source context 7 commands