Module

Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota

12 declarations indexed from sourceView source ↗

Module documentation

Tensoring the inclusion of an ideal module

Proves that tensoring the ideal inclusion by a locally free module preserves its monomorphism.

Imports5

Imported by5

lemma

mono_map_of_natIso

L55 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.mono_map_of_natIso

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section general
variable {C D : Type*} [Category C] [Category D]

Lean source · statement

lemma mono_map_of_natIso {F G : C ⥤ D} (e : F ≅ G) {A B : C} (f : A ⟶ B) [Mono (G.map f)] :
    Mono (F.map f)

instance

preservesColimit_tensorRight

L73 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.preservesColimit_tensorRight

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section monoidal
variable {C : Type*} [Category C] [Abelian C] [MonoidalCategory C] [SymmetricCategory C]
  [MonoidalClosed C]

Lean source · statement

instance preservesColimit_tensorRight (P : C) {J : Type*} [Category J] (K : J ⥤ C) :
    PreservesColimit K (tensorRight P)

lemma

mono_sigmaMap

L78 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.mono_sigmaMap

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section monoidal
variable {C : Type*} [Category C] [Abelian C] [MonoidalCategory C] [SymmetricCategory C]
  [MonoidalClosed C]
omit [MonoidalCategory C] [SymmetricCategory C] [MonoidalClosed C] in

Lean source · statement

lemma mono_sigmaMap {ι : Type*} [Finite ι] {f g : ι → C} (p : ∀ i, f i ⟶ g i) (hp : ∀ i, Mono (p i))
    [HasCoproduct f] [HasCoproduct g] :
    Mono (Limits.Sigma.map p)

lemma

mono_unit_whiskerLeft

L103 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.mono_unit_whiskerLeft

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section monoidal
variable {C : Type*} [Category C] [Abelian C] [MonoidalCategory C] [SymmetricCategory C]
  [MonoidalClosed C]
omit [Abelian C] [SymmetricCategory C] [MonoidalClosed C] in

Lean source · statement

lemma mono_unit_whiskerLeft {P Q : C} (h : P ⟶ Q) [Mono h] : Mono (𝟙_ C ◁ h)

lemma

mono_sigmaUnit_whiskerLeft

L112 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.mono_sigmaUnit_whiskerLeft

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section monoidal
variable {C : Type*} [Category C] [Abelian C] [MonoidalCategory C] [SymmetricCategory C]
  [MonoidalClosed C]

Lean source · full declaration

lemma mono_sigmaUnit_whiskerLeft {ι : Type*} [Finite ι] {P Q : C} (h : P ⟶ Q) [Mono h]
    [HasCoproduct (fun _ : ι => 𝟙_ C)] :
    Mono ((∐ fun _ : ι => 𝟙_ C) ◁ h) := by
  let f : ι → C := fun _ => 𝟙_ C
  let σP : (∐ fun b => (tensorRight P).obj (f b)) ⟶ (tensorRight P).obj (∐ f) := sigmaComparison
    (tensorRight P) f
  let σQ : (∐ fun b => (tensorRight Q).obj (f b)) ⟶ (tensorRight Q).obj (∐ f) := sigmaComparison
    (tensorRight Q) f
  let Sm : (∐ fun b => (tensorRight P).obj (f b)) ⟶ (∐ fun b => (tensorRight Q).obj (f b)) :=
    Limits.Sigma.map (fun _ => 𝟙_ C ◁ h)
  let wh : (tensorRight P).obj (∐ f) ⟶ (tensorRight Q).obj (∐ f) := (∐ f) ◁ h
  have hnat : Sm ≫ σQ = σP ≫ wh := by
    apply Limits.Sigma.hom_ext
    intro i
    have e1 : Sigma.ι (fun b => (tensorRight P).obj (f b)) i ≫ Sm =
        (𝟙_ C ◁ h) ≫ Sigma.ι (fun b => (tensorRight Q).obj (f b)) i :=
      Limits.Sigma.ι_map (fun _ => 𝟙_ C ◁ h) i
    have e2 : Sigma.ι (fun b => (tensorRight Q).obj (f b)) i ≫ σQ = (tensorRight Q).map (Sigma.ι f
      i) :=
      ι_comp_sigmaComparison (tensorRight Q) f i
    have e3 : Sigma.ι (fun b => (tensorRight P).obj (f b)) i ≫ σP = (tensorRight P).map (Sigma.ι f
      i) :=
      ι_comp_sigmaComparison (tensorRight P) f i
    have e4 : (𝟙_ C ◁ h) ≫ (tensorRight Q).map (Sigma.ι f i) = (tensorRight P).map (Sigma.ι f i) ≫
      wh :=
      whisker_exchange (Sigma.ι f i) h
    have L : Sigma.ι (fun b => (tensorRight P).obj (f b)) i ≫ (Sm ≫ σQ) =
        (𝟙_ C ◁ h) ≫ (tensorRight Q).map (Sigma.ι f i) :=
      ((Category.assoc _ _ _).symm.trans (congrArg (· ≫ σQ) e1)).trans
        ((Category.assoc _ _ _).trans (congrArg ((𝟙_ C ◁ h) ≫ ·) e2))
    have R : Sigma.ι (fun b => (tensorRight P).obj (f b)) i ≫ (σP ≫ wh) = (tensorRight P).map
      (Sigma.ι f i) ≫ wh :=
      (Category.assoc _ _ _).symm.trans (congrArg (· ≫ wh) e3)
    exact L.trans (e4.trans R.symm)
  have hσP : IsIso σP := inferInstance
  let σPinv : (tensorRight P).obj (∐ f) ⟶ (∐ fun b => (tensorRight P).obj (f b)) := inv σP
  have heq : wh = σPinv ≫ Sm ≫ σQ :=
    ((IsIso.inv_hom_id_assoc σP wh).symm).trans (congrArg (σPinv ≫ ·) hnat.symm)
  have hm : Mono Sm := mono_sigmaMap (f := fun b => (tensorRight P).obj (f b)) (g := fun b =>
    (tensorRight Q).obj (f b))
    (fun _ => 𝟙_ C ◁ h) (fun _ => mono_unit_whiskerLeft h)
  have hQ : Mono σQ := IsIso.mono_of_iso _
  have hP : Mono σPinv := IsIso.mono_of_iso _
  have hm2 : Mono (Sm ≫ σQ) := @mono_comp _ _ _ _ _ _ hm _ hQ
  have hfin : Mono (σPinv ≫ Sm ≫ σQ) := @mono_comp _ _ _ _ _ _ hP _ hm2
  have hwh : Mono wh := heq ▸ hfin
  exact hwh

lemma

mono_pullback_map_of_mono

L166 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.mono_pullback_map_of_mono

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section scheme
variable {X : Scheme.{u}}

Lean source · statement

lemma mono_pullback_map_of_mono (V : X.Opens) {M N : X.Modules} (φ : M ⟶ N) [Mono φ] :
    Mono ((Scheme.Modules.pullback V.ι).map φ)

lemma

image_preimage_eq_inf

L174 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.image_preimage_eq_inf

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section scheme
variable {X : Scheme.{u}}

Lean source · statement

lemma image_preimage_eq_inf (V U : X.Opens) : V.ι ''ᵁ (V.ι ⁻¹ᵁ U) = V ⊓ U

lemma

app_res

L177 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.app_res

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section scheme
variable {X : Scheme.{u}}

Lean source · statement

lemma app_res {M N : X.Modules} (φ : M ⟶ N) {W' W : X.Opens} (h : W' ≤ W) (s : Γ(M, W)) :
    φ.app W' (M.presheaf.map (homOfLE h).op s) = N.presheaf.map (homOfLE h).op (φ.app W s)

lemma

mono_of_forall_exists_mono_pullback

L184 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.mono_of_forall_exists_mono_pullback

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section scheme
variable {X : Scheme.{u}}

Lean source · statement

lemma mono_of_forall_exists_mono_pullback {M N : X.Modules} (φ : M ⟶ N)
    (h : ∀ x : X, ∃ V : X.Opens, x ∈ V ∧ Mono ((Scheme.Modules.pullback V.ι).map φ)) : Mono φ

theorem

mono_whiskerLeft_moduleι'

L206 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.MonoWhisker.mono_whiskerLeft_moduleι'

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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
namespace MonoWhisker
section scheme
variable {X : Scheme.{u}}

Lean source · statement

theorem mono_whiskerLeft_moduleι' (I : X.IdealSheafData) {n : ℕ} (F : X.Modules)
    (hF : Scheme.Modules.IsLocallyFreeOfRank n F) : Mono (F ◁ I.moduleι)

theorem

mono_whiskerLeft_moduleι

L248 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota.AlgebraicGeometry.Scheme.IdealSheafData.mono_whiskerLeft_moduleι

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
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

Lean source · statement

theorem mono_whiskerLeft_moduleι {X : Scheme.{u}} (I : X.IdealSheafData) {n : ℕ} (F : X.Modules)
    (hF : Scheme.Modules.IsLocallyFreeOfRank n F) : Mono (F ◁ I.moduleι)

theorem

mono_whiskerLeft_moduleIota

L254 ↗

AlgebraicGeometry.Scheme.IdealSheafData.mono_whiskerLeft_moduleIota

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_IdealSheafData_mono_whiskerLeft_moduleIota
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.IdealSheafData.mono_whiskerLeft_moduleIota {X :
  Scheme.{u}} (I : X.IdealSheafData) {n : ℕ} (F : X.Modules)
    (hF : Scheme.Modules.IsLocallyFreeOfRank n F) : Mono (F ◁ I.moduleι)

Module documentation

Tensoring the inclusion of an ideal module

Declarations