Module

Scheme_IdealSheafData_comap_ofIdealTop.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_comap_ofIdealTop

1 declaration indexed from sourceView source ↗

Module documentation

Scheme Ideal Sheaf Data comap of Ideal Top

Imports2

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_ideal_comap_of_le

Imported by2

theorem

comap_ofIdealTop

L28 ↗

AlgebraicGeometry.Scheme.IdealSheafData.comap_ofIdealTop

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_ofIdealTop
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.comap_ofIdealTop
    {X Y : Scheme.{u}} (I : Ideal Γ(Y, ⊤)) (f : X ⟶ Y) :
    (Scheme.IdealSheafData.ofIdealTop I).comap f
      = Scheme.IdealSheafData.ofIdealTop (I.map f.appTop.hom)

Module documentation

Scheme Ideal Sheaf Data comap of Ideal Top

Declarations

comap_ofIdealTop