NYLL
Module

Scheme_IdealSheafData_ideal_comap_of_le.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_ideal_comap_of_le
6 declarations indexed from sourceView source ↗

Module documentation

Affine ideals of an inverse image

The inverse image of an ideal sheaf is computed on affine opens by extension of the original ideal along the induced homomorphism on sections.

Imports12
  • Mathlib.Util.WithWeakNamespace
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.Algebra.Algebra.Hom
  • Mathlib.AlgebraicGeometry.Morphisms.Flat
  • Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
  • Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  • Mathlib.RingTheory.RingHom.Flat
  • Mathlib.RingTheory.LocalProperties.Basic
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
  • Mathlib.Algebra.Category.Ring.Constructions
  • Mathlib.LinearAlgebra.TensorProduct.RightExactness
  • Mathlib.RingTheory.IsTensorProduct
Imported by8

Declarations

theorem

ker_algebraMap_eq_map_ker

L48 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le.Algebra.IsPushout.ker_algebraMap_eq_map_ker
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace Algebra
open _root_.Algebra
namespace IsPushout
open _root_.Algebra.IsPushout
open _root_.Algebra.IsPushout
open _root_.Algebra
Lean source · statement
theorem 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

ker_eq_map_ker_of_isPushout

L91 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le.CommRingCat.ker_eq_map_ker_of_isPushout
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace CommRingCat
open _root_.CommRingCat
open _root_.CommRingCat
Lean source · statement
theorem 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

ideal_comap_top

L118 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le.AlgebraicGeometry.Scheme.IdealSheafData.ComapLocal.ideal_comap_top
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace ComapLocal
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
variable {X Y : Scheme.{u}}
Lean source · statement
theorem 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

ideal_comap_of_le

L129 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le.AlgebraicGeometry.Scheme.IdealSheafData.ComapLocal.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.Scheme_IdealSheafData_ideal_comap_of_le
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace ComapLocal
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
variable {X Y : Scheme.{u}}
Lean source · statement
theorem 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
theorem

ideal_comap_of_isAffineHom

L153 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le.AlgebraicGeometry.Scheme.IdealSheafData.ComapLocal.ideal_comap_of_isAffineHom
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace IdealSheafData
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
namespace ComapLocal
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
variable {X Y : Scheme.{u}}
Lean source · statement
theorem ideal_comap_of_isAffineHom (I : X.IdealSheafData) (f : Y ⟶ X) [IsAffineHom f]
    (U : X.affineOpens) :
    (I.comap f).ideal ⟨f ⁻¹ᵁ U, U.2.preimage f⟩ = (I.ideal U).map (f.app U).hom
theorem

ideal_comap_of_le

L165 ↗
AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_le
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_ideal_comap_of_le
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
with_weak_namespace _root_.AlgebraicCurves.Geometry.Sheaves.Proofs
open CategoryTheory _root_.AlgebraicGeometry
    Scheme_IdealSheafData_ideal_comap_of_le.AlgebraicGeometry in
with_weak_namespace Scheme_IdealSheafData_ideal_comap_of_le
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_le
    {X Y : Scheme.{u}} (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

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