NYLL
Module

Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
9 declarations indexed from sourceView source ↗

Module documentation

Local surjectivity of the ideal-module pullback comparison

The canonical map from a pulled-back ideal module to the inverse-image ideal module is locally surjective.

Imports5
Imported by2

Declarations

theorem

lbE_ker_algebraMap_eq_map_ker

L44 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective.Algebra.IsPushout.lbE_ker_algebraMap_eq_map_ker
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace Algebra
open _root_.Algebra
namespace IsPushout
open _root_.Algebra.IsPushout
open _root_.Algebra.IsPushout
open _root_.Algebra
Lean source · statement
theorem lbE_ker_algebraMap_eq_map_ker
    (R B C P : Type*) [CommRing R] [CommRing B] [CommRing C] [CommRing P]
    [Algebra R B] [Algebra R C] [Algebra B P] [Algebra C P] [Algebra R P]
    [IsScalarTower R B P] [IsScalarTower R C P] [Algebra.IsPushout R B C P]
    (hC : Function.Surjective (algebraMap R C)) :
    RingHom.ker (algebraMap B P) = (RingHom.ker (algebraMap R C)).map (algebraMap R B)
theorem

lbE_ker_eq_map_ker_of_isPushout

L87 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective.CommRingCat.lbE_ker_eq_map_ker_of_isPushout
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace CommRingCat
open _root_.CommRingCat
open _root_.CommRingCat
Lean source · statement
theorem lbE_ker_eq_map_ker_of_isPushout {R B C P : CommRingCat.{u}} {f : R ⟶ B} {g : R ⟶ C}
    {inl : B ⟶ P} {inr : C ⟶ P} (h : IsPushout f g inl inr)
    (hg : Function.Surjective g.hom) :
    RingHom.ker inl.hom = (RingHom.ker g.hom).map f.hom
theorem

lbE_ideal_comap_top

L112 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective.AlgebraicGeometry.Scheme.IdealSheafData.lbE_ideal_comap_top
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}
Lean source · statement
theorem lbE_ideal_comap_top [IsAffine X] [IsAffine Y] (I : X.IdealSheafData) (f : Y ⟶ X) :
    (I.comap f).ideal ⟨⊤, isAffineOpen_top Y⟩ =
      (I.ideal ⟨⊤, isAffineOpen_top X⟩).map f.appTop.hom
theorem

lbE_ideal_comap_of_le

L123 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective.AlgebraicGeometry.Scheme.IdealSheafData.lbE_ideal_comap_of_le
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}
Lean source · statement
theorem lbE_ideal_comap_of_le (I : X.IdealSheafData) (f : Y ⟶ X) (U : X.affineOpens)
    (V : Y.affineOpens) (hVU : (V : Y.Opens) ≤ f ⁻¹ᵁ (U : X.Opens)) :
    (I.comap f).ideal V = (I.ideal U).map (f.appLE U V hVU).hom
instance

pullbackComparisonRightAdjoint

L171 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective.AlgebraicGeometry.Scheme.IdealSheafData.pullbackComparisonRightAdjoint
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
Lean source · statement
instance pullbackComparisonRightAdjoint {X X' : Scheme.{u}} (f : X' ⟶ X) :
    (SheafOfModules.pushforward.{u}
      (F := TopologicalSpace.Opens.map f.base)
      (J := _root_.Opens.grothendieckTopology X)
      (K := _root_.Opens.grothendieckTopology X') f.toRingCatSheafHom).IsRightAdjoint
lemma

moduleToPushforwardComapModule_comp_map_moduleι

L178 ↗
AlgebraicGeometry.Scheme.IdealSheafData.moduleToPushforwardComapModule_comp_map_moduleι
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
local instance pullbackComparisonRightAdjoint {X X' : Scheme.{u}} (f : X' ⟶ X) :
    (SheafOfModules.pushforward.{u}
      (F := TopologicalSpace.Opens.map f.base)
      (J := _root_.Opens.grothendieckTopology X)
      (K := _root_.Opens.grothendieckTopology X') f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
Lean source · statement
lemma
    _root_.AlgebraicGeometry.Scheme.IdealSheafData.moduleToPushforwardComapModule_comp_map_moduleι
    {X X' : Scheme.{u}} (f : X' ⟶ X)
    (I : X.IdealSheafData) :
    I.moduleToPushforwardComapModule f ≫
        (SheafOfModules.pushforward f.toRingCatSheafHom).map
          (kernel.ι (I.comap f).subschemeι.unitToPushforwardUnit) =
      kernel.ι I.subschemeι.unitToPushforwardUnit ≫ f.unitToPushforwardUnit
lemma

unit_comp_map_pullbackModuleComparison

L195 ↗
AlgebraicGeometry.Scheme.IdealSheafData.unit_comp_map_pullbackModuleComparison
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
local instance pullbackComparisonRightAdjoint {X X' : Scheme.{u}} (f : X' ⟶ X) :
    (SheafOfModules.pushforward.{u}
      (F := TopologicalSpace.Opens.map f.base)
      (J := _root_.Opens.grothendieckTopology X)
      (K := _root_.Opens.grothendieckTopology X') f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
lemma _root_.AlgebraicGeometry.Scheme.IdealSheafData.unit_comp_map_pullbackModuleComparison
    {X X' : Scheme.{u}} (f : X' ⟶ X)
    (I : X.IdealSheafData) :
    (SheafOfModules.pullbackPushforwardAdjunction f.toRingCatSheafHom).unit.app
        (I.module : SheafOfModules X.ringCatSheaf) ≫
      (SheafOfModules.pushforward f.toRingCatSheafHom).map (I.pullbackModuleComparison f) =
      I.moduleToPushforwardComapModule f
theorem

lbE_pullbackModuleComparison_locallySurjective

L210 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective.AlgebraicGeometry.Scheme.IdealSheafData.lbE_pullbackModuleComparison_locallySurjective
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open Opposite TopologicalSpace
local instance pullbackComparisonRightAdjoint {X X' : Scheme.{u}} (f : X' ⟶ X) :
    (SheafOfModules.pushforward.{u}
      (F := TopologicalSpace.Opens.map f.base)
      (J := _root_.Opens.grothendieckTopology X)
      (K := _root_.Opens.grothendieckTopology X') f.toRingCatSheafHom).IsRightAdjoint :=
  (Scheme.Modules.pullbackPushforwardAdjunction f).isRightAdjoint
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem lbE_pullbackModuleComparison_locallySurjective {X X' : Scheme.{u}} (f : X' ⟶ X)
    (I : X.IdealSheafData) :
    ∀ (U : X'.Opens) (s : Γ((I.comap f).module, U)), ∀ x ∈ U,
      ∃ (V : X'.Opens) (i : V ≤ U), x ∈ V ∧
        ((I.comap f).module).presheaf.map (homOfLE i).op s ∈
          Set.range ((I.pullbackModuleComparison f).app V)
theorem

pullbackModuleComparison_locallySurjective

L281 ↗
AlgebraicGeometry.Scheme.IdealSheafData.pullbackModuleComparison_locallySurjective
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_IdealSheafData_pullbackModuleComparison_locallySurjective
universe u
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
open _root_.AlgebraicGeometry AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.pullbackModuleComparison_locallySurjective {X
  X' : Scheme.{u}} (f : X' ⟶ X) (I : X.IdealSheafData) :
    ∀ (U : X'.Opens) (s : Γ((I.comap f).module, U)), ∀ x ∈ U,
      ∃ (V : X'.Opens) (i : V ≤ U), x ∈ V ∧
        ((I.comap f).module).presheaf.map (homOfLE i).op s ∈
          Set.range ((I.pullbackModuleComparison f).app V)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.