Module

IdealSheafHom.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafHom

37 declarations indexed from sourceView source ↗

Module documentation

Morphisms of ideal-sheaf data

Compatible linear maps on ideals over affine opens admit module operations, composition, and ideal-sheaf ranges.

Imports1

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Imported by2

def

sres

L33 ↗

AlgebraicGeometry.Scheme.IdealSheafData.sres

Documentation

The restriction homomorphism of regular functions along an inclusion of affine opens.

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · statement

def sres {U V : X.affineOpens} (h : V ≤ U) : Γ(X, U) →+* Γ(X, V)

def

sresTop

L37 ↗

AlgebraicGeometry.Scheme.IdealSheafData.sresTop

Documentation

Restrict a global regular function to the affine open U.

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · statement

def sresTop (U : X.affineOpens) : Γ(X, ⊤) →+* Γ(X, U)

lemma

sres_apply

L40 ↗

AlgebraicGeometry.Scheme.IdealSheafData.sres_apply

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · full declaration

lemma sres_apply {U V : X.affineOpens} (h : V ≤ U) (s : Γ(X, U)) :
    sres h s = (X.presheaf.map (homOfLE (show (V : X.Opens) ≤ U from h)).op).hom s := rfl

lemma

sresTop_apply

L43 ↗

AlgebraicGeometry.Scheme.IdealSheafData.sresTop_apply

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · statement

lemma sresTop_apply (U : X.affineOpens) (s : Γ(X, ⊤)) :
    sresTop U s = (X.presheaf.map (homOfLE (le_top : (U : X.Opens) ≤ ⊤)).op).hom s

lemma

sres_sresTop

L46 ↗

AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · statement

lemma sres_sresTop {U V : X.affineOpens} (h : V ≤ U) (s : Γ(X, ⊤)) :
    sres h (sresTop U s) = sresTop V s

lemma

sres_sres

L51 ↗

AlgebraicGeometry.Scheme.IdealSheafData.sres_sres

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · statement

lemma sres_sres {U V W : X.affineOpens} (h : W ≤ V) (h' : V ≤ U) (s : Γ(X, U)) :
    sres h (sres h' s) = sres (h.trans h') s

def

resLE

L57 ↗

AlgebraicGeometry.Scheme.IdealSheafData.resLE

Documentation

Restrict an element of the ideal on U to the ideal on the affine open V.

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · statement

def resLE (I : X.IdealSheafData) {U V : X.affineOpens} (h : V ≤ U) (x : I.ideal U) :
    I.ideal V

lemma

coe_resLE

L61 ↗

AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · statement

lemma coe_resLE (I : X.IdealSheafData) {U V : X.affineOpens} (h : V ≤ U)
    (x : I.ideal U) : (I.resLE h x : Γ(X, V)) = sres h (x : Γ(X, U))

structure

IdealHom

L65 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom

Documentation

A family of linear maps between the ideals on affine opens, compatible with restriction.

Source context 5 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData

Lean source · full declaration

structure IdealHom (I J : X.IdealSheafData) : Type u where
  /-- The linear map on each affine open. -/
  app : ∀ U : X.affineOpens, I.ideal U →ₗ[Γ(X, U)] J.ideal U
  /-- Restricting an input and then applying `app` agrees, as a regular function, with restricting
    its image. -/
  coe_app_resLE : ∀ {U V : X.affineOpens} (h : V ≤ U) (x : I.ideal U),
    ((app V (I.resLE h x) : J.ideal V) : Γ(X, V)) = sres h ((app U x : J.ideal U) : Γ(X, U))

lemma

ext

L78 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ext

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma ext {φ ψ : IdealHom I J} (h : φ.app = ψ.app) : φ = ψ

instance

(anonymous instance)

L81 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : Zero (IdealHom I J)

instance

(anonymous instance)

L82 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : Add (IdealHom I J)

instance

(anonymous instance)

L86 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : Neg (IdealHom I J)

instance

(anonymous instance)

L89 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : Sub (IdealHom I J)

instance

(anonymous instance)

L93 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : SMul ℕ (IdealHom I J)

instance

(anonymous instance)

L97 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : SMul ℤ (IdealHom I J)

lemma

zero_app

L102 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma zero_app (U : X.affineOpens) : (0 : IdealHom I J).app U = 0

lemma

add_app

L103 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma add_app (φ ψ : IdealHom I J) (U : X.affineOpens) :
    (φ + ψ).app U = φ.app U + ψ.app U

lemma

neg_app

L105 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma neg_app (φ : IdealHom I J) (U : X.affineOpens) : (-φ).app U = -φ.app U

lemma

sub_app

L106 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma sub_app (φ ψ : IdealHom I J) (U : X.affineOpens) :
    (φ - ψ).app U = φ.app U - ψ.app U

lemma

nsmul_app

L108 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma nsmul_app (n : ℕ) (φ : IdealHom I J) (U : X.affineOpens) :
    (n • φ).app U = n • φ.app U

lemma

zsmul_app

L110 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma zsmul_app (n : ℤ) (φ : IdealHom I J) (U : X.affineOpens) :
    (n • φ).app U = n • φ.app U

instance

(anonymous instance)

L113 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : AddCommGroup (IdealHom I J)

instance

(anonymous instance)

L118 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

instance : SMul Γ(X, ⊤) (IdealHom I J)

lemma

smul_app

L123 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma smul_app (s : Γ(X, ⊤)) (φ : IdealHom I J) (U : X.affineOpens) :
    (s • φ).app U = sresTop U s • φ.app U

instance

(anonymous instance)

L126 ↗

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · full declaration

instance : Module Γ(X, ⊤) (IdealHom I J) where
  one_smul φ := by ext U x; simp
  mul_smul r s φ := by ext U x; simp [mul_smul]
  smul_zero r := by ext U x; simp
  smul_add r φ ψ := by ext U x; simp
  add_smul r s φ := by ext U x; simp [add_smul]
  zero_smul φ := by ext U x; simp

def

ofLE

L135 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ofLE

Documentation

The morphism induced by inclusion of ideal sheaf data.

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · full declaration

def ofLE (h : I ≤ J) : IdealHom I J where
  app U := Submodule.inclusion (le_def.mp h U)
  coe_app_resLE _ _ := rfl

lemma

coe_ofLE_app

L139 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma coe_ofLE_app (h : I ≤ J) (U : X.affineOpens) (x : I.ideal U) :
    ((ofLE h).app U x : Γ(X, U)) = x

def

id

L143 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id

Documentation

The identity morphism of ideal sheaf data.

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

def id (I : X.IdealSheafData) : IdealHom I I

lemma

id_app

L145 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma id_app (I : X.IdealSheafData) (U : X.affineOpens) (x : I.ideal U) :
    (IdealHom.id I).app U x = x

def

comp

L149 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp

Documentation

Compose morphisms of ideal sheaf data on each affine open.

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · full declaration

def comp (ψ : IdealHom J K) (φ : IdealHom I J) : IdealHom I K where
  app U := ψ.app U ∘ₗ φ.app U
  coe_app_resLE := by
    intro U V h x
    have h₁ : φ.app V (I.resLE h x) = J.resLE h (φ.app U x) := Subtype.ext (φ.coe_app_resLE h x)
    simp only [LinearMap.coe_comp, Function.comp_apply, h₁, ψ.coe_app_resLE h]

lemma

comp_app

L156 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma comp_app (ψ : IdealHom J K) (φ : IdealHom I J) (U : X.affineOpens)
    (x : I.ideal U) : (ψ.comp φ).app U x = ψ.app U (φ.app U x)

def

mulRight

L160 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mulRight

Documentation

Multiply sections of I by restrictions of s, producing sections of I * J using hs.

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · full declaration

def mulRight (I J : X.IdealSheafData) (s : Γ(X, ⊤))
    (hs : ∀ U : X.affineOpens, sresTop U s ∈ J.ideal U) : IdealHom I (I * J) where
  app U :=
    { toFun := fun x => ⟨x * sresTop U s, by rw [ideal_mul]; exact Ideal.mul_mem_mul x.2 (hs U)⟩
      map_add' := fun x y => Subtype.ext (add_mul _ _ _)
      map_smul' := fun r x => Subtype.ext (mul_assoc _ _ _) }
  coe_app_resLE := by
    intro U V h x
    change sres h (x : Γ(X, U)) * sresTop V s = sres h ((x : Γ(X, U)) * sresTop U s)
    rw [map_mul, sres_sresTop]

lemma

coe_mulRight_app

L171 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma coe_mulRight_app (I J : X.IdealSheafData) (s : Γ(X, ⊤))
    (hs : ∀ U : X.affineOpens, sresTop U s ∈ J.ideal U) (U : X.affineOpens) (x : I.ideal U) :
    ((mulRight I J s hs).app U x : Γ(X, U)) = x * sresTop U s

def

range

L178 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.range

Documentation

The ideal sheaf data whose ideal on an affine open is the image of φ.app in the ring of regular functions.

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · full declaration

def range (φ : IdealHom I J) : X.IdealSheafData where
  ideal U := LinearMap.range ((J.ideal U).subtype ∘ₗ φ.app U)
  map_ideal_basicOpen U f := by
    have hle : X.affineBasicOpen f ≤ U := X.affineBasicOpen_le f
    change Ideal.map (sres hle)
      (LinearMap.range ((J.ideal U).subtype ∘ₗ φ.app U)) =
        LinearMap.range
          ((J.ideal (X.affineBasicOpen f)).subtype ∘ₗ φ.app (X.affineBasicOpen f))
    apply le_antisymm
    · rw [Ideal.map_le_iff_le_comap]
      rintro _ ⟨x, rfl⟩
      exact ⟨I.resLE hle x, (φ.coe_app_resLE hle x)⟩
    · rintro _ ⟨y, rfl⟩
      let M : Submodule (Γ(X, X.affineBasicOpen f)) (I.ideal (X.affineBasicOpen f)) :=
        Submodule.comap ((J.ideal _).subtype ∘ₗ φ.app _)
          (Ideal.map (sres hle) (LinearMap.range ((J.ideal U).subtype ∘ₗ φ.app U)))
      suffices h : y ∈ M by rw [Submodule.mem_comap] at h; exact h
      have hle' : (I.ideal U).map (sres hle) ≤ M.map (I.ideal _).subtype := by
        rw [Ideal.map_le_iff_le_comap]
        intro x hx
        refine ⟨I.resLE hle ⟨x, hx⟩, ?_, rfl⟩
        rw [SetLike.mem_coe, Submodule.mem_comap, LinearMap.comp_apply, Submodule.subtype_apply,
          φ.coe_app_resLE]
        exact Ideal.mem_map_of_mem (sres hle)
          (LinearMap.mem_range.mpr ⟨⟨x, hx⟩, rfl⟩ : ((φ.app U ⟨x, hx⟩ : J.ideal U) : Γ(X, U)) ∈
            LinearMap.range ((J.ideal U).subtype ∘ₗ φ.app U))
      have hy : (y : Γ(X, X.affineBasicOpen f)) ∈ (I.ideal U).map (sres hle) :=
        (I.map_ideal_basicOpen U f).ge y.2
      obtain ⟨y', hy', hyy'⟩ := hle' hy
      have : y' = y := Subtype.ext hyy'
      exact this ▸ hy'

lemma

ideal_range

L210 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma ideal_range (φ : IdealHom I J) (U : X.affineOpens) :
    φ.range.ideal U = LinearMap.range ((J.ideal U).subtype ∘ₗ φ.app U)

lemma

range_le

L213 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.range_le

Source context 7 commands

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

open CategoryTheory TopologicalSpace Opposite
universe u
namespace AlgebraicGeometry.Scheme
variable {X : Scheme.{u}}
namespace IdealSheafData
namespace IdealHom
variable {I J K : X.IdealSheafData}

Lean source · statement

lemma range_le (φ : IdealHom I J) : φ.range ≤ J

Module documentation

Morphisms of ideal-sheaf data

Declarations