Module

Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover

4 declarations indexed from sourceView source ↗

Module documentation

Scheme Ideal Sheaf Data Is Invertible of forall comap open Cover

Imports6

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Mathlib.RingTheory.Ideal.Maps
Nyll.AlgebraicCurves.RelativeDivisors.Cartier

Imported by3

theorem

image_basicOpen_eq

L37 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover.INVLOCALCOVER.image_basicOpen_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace INVLOCALCOVER
variable {W X : Scheme.{u}} (j : W ⟶ X) [IsOpenImmersion j] (I : X.IdealSheafData)

Lean source · statement

theorem image_basicOpen_eq (U : W.Opens) (f : Γ(W, U)) :
    j ''ᵁ (W.basicOpen f) = X.basicOpen ((j.appIso U).inv.hom f)

theorem

at_image

L47 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover.INVLOCALCOVER.at_image

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace INVLOCALCOVER
variable {W X : Scheme.{u}} (j : W ⟶ X) [IsOpenImmersion j] (I : X.IdealSheafData)

Lean source · statement

theorem at_image (h : (I.comap j).IsInvertible) (w : W) :
    ∃ (U : X.affineOpens) (f : Γ(X, U)), j w ∈ X.basicOpen f ∧
      ∃ g ∈ nonZeroDivisors Γ(X, X.affineBasicOpen f), I.ideal (X.affineBasicOpen f) = Ideal.span
        {g}

theorem

main

L84 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover.INVLOCALCOVER.main

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
namespace INVLOCALCOVER
variable {W X : Scheme.{u}} (j : W ⟶ X) [IsOpenImmersion j] (I : X.IdealSheafData)

Lean source · statement

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

theorem

of_forall_comap_openCover

L92 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.of_forall_comap_openCover

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_IsInvertible_of_forall_comap_openCover
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.of_forall_comap_openCover
    {X : Scheme.{u}} (𝒰 : X.OpenCover) (I : X.IdealSheafData)
    (h : ∀ i, (I.comap (𝒰.f i)).IsInvertible) : I.IsInvertible

Module documentation

Scheme Ideal Sheaf Data Is Invertible of forall comap open Cover

Declarations

image_basicOpen_eq

at_image

main

of_forall_comap_openCover