Module

FiniteTypeCoprod.lean

Nyll.SchemeTheory.Modules.FiniteTypeCoprod

6 declarations indexed from sourceView source ↗

Module documentation

Finite type of binary coproducts

The product of the two original local generating covers is again a cover. On each product chart both finite generating families restrict, and their disjoint union generates the actual categorical coproduct.

Imports7

Nyll.SchemeTheory.Modules.FiniteTypeQuotient
Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
Mathlib.CategoryTheory.Limits.Preserves.Finite
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryProducts
Mathlib.Basic.Finite.Sum

Imported by2

def

coprod

L36 ↗

SheafOfModules.GeneratingSections.coprod

Documentation

Generators of both summands give generators indexed by their disjoint union.

Source context 5 commands

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

noncomputable section
universe u v u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · full declaration

def GeneratingSections.coprod {M N : SheafOfModules.{u} R}
    (p : M.GeneratingSections) (q : N.GeneratingSections) :
    (M ⨿ N).GeneratingSections where
  I := p.I ⊕ q.I
  s := (M ⨿ N).freeHomEquiv
    ((freeSumIso (R := R) p.I q.I).inv ≫ Limits.coprod.map p.π q.π)
  epi := by
    rw [Equiv.symm_apply_apply]
    infer_instance

instance

(anonymous instance)

L46 ↗

Source context 5 commands

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

noncomputable section
universe u v u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · full declaration

instance {M N : SheafOfModules.{u} R}
    (p : M.GeneratingSections) (q : N.GeneratingSections)
    [p.IsFiniteType] [q.IsFiniteType] : (p.coprod q).IsFiniteType where
  finite := inferInstanceAs (Finite (p.I ⊕ q.I))

def

restrict

L56 ↗

SheafOfModules.GeneratingSections.restrict

Documentation

Restrict a generating family further along a map of charts.

Source context 6 commands

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

noncomputable section
universe u v u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
variable [HasBinaryProducts C] [HasPullbacks C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

def GeneratingSections.restrict {M : SheafOfModules.{u} R} {X Y : C}
    (p : (M.over Y).GeneratingSections) (f : X ⟶ Y) :
    (M.over X).GeneratingSections

instance

(anonymous instance)

L62 ↗

Source context 6 commands

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

noncomputable section
universe u v u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
variable [HasBinaryProducts C] [HasPullbacks C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

instance {M : SheafOfModules.{u} R} {X Y : C}
    (p : (M.over Y).GeneratingSections) (f : X ⟶ Y) [p.IsFiniteType] :
    (p.restrict f).IsFiniteType

def

coprodChartGenerators

L69 ↗

SheafOfModules.coprodChartGenerators

Source context 6 commands

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

noncomputable section
universe u v u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
variable [HasBinaryProducts C] [HasPullbacks C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

def coprodChartGenerators {M N : SheafOfModules.{u} R}
    (p : M.LocalGeneratorsData) (q : N.LocalGeneratorsData) (i : p.I) (j : q.I) :
    ((M ⨿ N).over (p.X i ⨯ q.X j)).GeneratingSections

theorem

isFiniteType_coprod

L81 ↗

SheafOfModules.isFiniteType_coprod

Documentation

The actual binary coproduct of two finite-type sheaves is finite type.

Source context 6 commands

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

noncomputable section
universe u v u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [HasSheafify J AddCommGrpCat.{u}] [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
variable [HasBinaryProducts C] [HasPullbacks C]
  [∀ X : C, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X : C, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

theorem isFiniteType_coprod {M N : SheafOfModules.{u} R}
    [M.IsFiniteType] [N.IsFiniteType] : (M ⨿ N).IsFiniteType

Module documentation

Finite type of binary coproducts

Declarations

coprod

(anonymous instance)

restrict

(anonymous instance)

coprodChartGenerators

isFiniteType_coprod