SheafOfModules.LocalGeneratorsData.over
Restrict local generators using all objects which map into the original cover.
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] [HasPullbacks C]
{J : GrothendieckTopology C} {R : Sheaf J RingCat.{u}}
[∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
[∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
[∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
[∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]Lean source · full declaration
def LocalGeneratorsData.over {M : SheafOfModules.{u} R}
(q : M.LocalGeneratorsData) (U : C) : (M.over U).LocalGeneratorsData where
I := (V : Over U) × (i : q.I) × (V.left ⟶ q.X i)
X i := i.1
coversTop Y := by
apply (J.over U).superset_covering _
((Over.forget U).cover_lift (J.over U) J (q.coversTop Y.left))
intro Z g hg
obtain ⟨i, ⟨v⟩⟩ := hg
exact ⟨⟨Z, i, v⟩, ⟨𝟙 Z⟩⟩
generators i := by
let t := (q.generators i.2.1).map (overMap R i.2.2)
(overMapUnitIso (R := R) i.2.2).symm
let t' : (M.over i.1.left).GeneratingSections :=
t.ofEpi ((overFunctorMap R i.2.2).app M).hom
let e := pushforwardPushforwardEquivalence (Over.iteratedSliceEquiv i.1)
(S := (R.over U).over i.1) (R := R.over i.1.left) (𝟙 _) (𝟙 _)
(by ext : 2; exact R.1.map_id _) (by ext : 2; exact R.1.map_id _)
exact t'.map e.functor (Iso.refl _)