Module

Scheme_IdealSheafData_comap_mul.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_comap_mul

5 declarations indexed from sourceView source ↗

Module documentation

Inverse image and multiplication of ideal sheaves

The product of ideal-sheaf data commutes with inverse image along a scheme morphism.

Imports4

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.Algebra.Category.Ring.Constructions
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.RingTheory.IsTensorProduct

Imported by29

theorem

w2a3_ker_algebraMap_eq_map_ker

L39 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_mul.Algebra.IsPushout.w2a3_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_comap_mul
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 w2a3_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

w2a3_ker_eq_map_ker_of_isPushout

L82 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_mul.CommRingCat.w2a3_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_comap_mul
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
namespace CommRingCat
open _root_.CommRingCat
open _root_.CommRingCat

Lean source · statement

theorem w2a3_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

w2a3_ideal_comap_top

L107 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_mul.AlgebraicGeometry.Scheme.IdealSheafData.w2a3_ideal_comap_top

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_mul
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
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

theorem w2a3_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

w2a3_ideal_comap_of_le

L118 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_mul.AlgebraicGeometry.Scheme.IdealSheafData.w2a3_ideal_comap_of_le

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_mul
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
open _root_.AlgebraicGeometry.Scheme.IdealSheafData
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {X Y : Scheme.{u}}

Lean source · statement

theorem w2a3_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

comap_mul

L156 ↗

AlgebraicGeometry.Scheme.IdealSheafData.comap_mul

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_comap_mul
universe u
open CategoryTheory CategoryTheory.Limits TensorProduct
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.comap_mul {X Y : Scheme.{u}}
    (I J : Y.IdealSheafData) (f : X ⟶ Y) :
    (I * J).comap f = I.comap f * J.comap f

Module documentation

Inverse image and multiplication of ideal sheaves

Declarations

w2a3_ker_algebraMap_eq_map_ker

w2a3_ker_eq_map_ker_of_isPushout

w2a3_ideal_comap_top

w2a3_ideal_comap_of_le

comap_mul