Module

Scheme_IdealSheafData_exists_iso_subscheme_comap_of_support_subset_range.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_exists_iso_subscheme_comap_of_support_subset_range

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Ideal Sheaf Data exists iso subscheme comap of support subset range

Imports3

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.AlgebraicGeometry.PullbackCarrier

Imported by3

theorem

exists_iso_subscheme_comap_of_support_subset_range

L30 ↗

AlgebraicGeometry.Scheme.IdealSheafData.exists_iso_subscheme_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_exists_iso_subscheme_comap_of_support_subset_range
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.IdealSheafData.exists_iso_subscheme_comap_of_support_subset_range
    {X Y : Scheme.{u}} (I : X.IdealSheafData) (ψ : Y ⟶ X) [IsOpenImmersion ψ]
    (h : (I.support : Set X) ⊆ Set.range ψ) :
    ∃ e : (I.comap ψ).subscheme ≅ I.subscheme, e.hom ≫ I.subschemeι = (I.comap ψ).subschemeι ≫ ψ

Module documentation

Scheme Ideal Sheaf Data exists iso subscheme comap of support subset range

Declarations

exists_iso_subscheme_comap_of_support_subset_range