Module

Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range

4 declarations indexed from sourceView source ↗

Module documentation

Scheme Ideal Sheaf Data Is Invertible of comap of support subset range

Imports3

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.Tactic.Push
Nyll.AlgebraicCurves.RelativeDivisors.Cartier

Imported by7

theorem

exists_of_not_mem_support

L34 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range.InvLocal.exists_of_not_mem_support

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_comap_of_support_subset_range
universe u
namespace InvLocal
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
variable {W X : Scheme.{u}} (j : W ⟶ X) [IsOpenImmersion j] (I : X.IdealSheafData)

Lean source · statement

theorem exists_of_not_mem_support (x : X) (hx : x ∉ I.support) :
    ∃ (U : X.affineOpens) (f : Γ(X, U)), x ∈ X.basicOpen f ∧
      ∃ g ∈ nonZeroDivisors Γ(X, X.affineBasicOpen f), I.ideal (X.affineBasicOpen f) = Ideal.span
        {g}

theorem

image_basicOpen_eq

L50 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range.InvLocal.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_comap_of_support_subset_range
universe u
namespace InvLocal
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
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

main

L60 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range.InvLocal.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_comap_of_support_subset_range
universe u
namespace InvLocal
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace Opposite
variable {W X : Scheme.{u}} (j : W ⟶ X) [IsOpenImmersion j] (I : X.IdealSheafData)

Lean source · statement

theorem main
    {W X : Scheme.{u}} (j : W ⟶ X) [IsOpenImmersion j] (I : X.IdealSheafData)
    (hsupp : (I.support : Set ↥X) ⊆ Set.range ⇑j) (h : (I.comap j).IsInvertible) :
    I.IsInvertible

theorem

of_comap_of_support_subset_range

L105 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.of_comap_of_support_subset_range

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_comap_of_support_subset_range
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.of_comap_of_support_subset_range
    {W X : Scheme.{u}} (j : W ⟶ X) [IsOpenImmersion j] (I : X.IdealSheafData)
    (hsupp : (I.support : Set ↥X) ⊆ Set.range ⇑j) (h : (I.comap j).IsInvertible) :
    I.IsInvertible

Module documentation

Scheme Ideal Sheaf Data Is Invertible of comap of support subset range

Declarations

exists_of_not_mem_support

image_basicOpen_eq

main

of_comap_of_support_subset_range