English
Let G: C → D be a functor that preserves compatibility with respect to a Grothendieck topology K on D, and let ℱ be a sheaf on D. For any Z, T on Z, and any x ∈ FamilyOfElements (G^op ∘ ℱ.val) T that is Compatible, the pushforward (x.functorPushforward G) is again a Compatible family.
Русский
Пусть G: C → D — функтор, сохраняющий совместимость относительно топологии К на D, и ℱ — она на D. Для любой Z, Presieve T на Z, и для любого x ∈ FamilyOfElements (G^op ∘ ℱ.val) T, являющегося совместимым, отображение x.functorPushforward G также образует совместную семью.
LaTeX
$$$\forall {C} {D} [Category C] [Category D] (K : GrothendieckTopology D) (G : C ⥤ D)
(hG : CompatiblePreserving K G) (\ℱ : Sheaf K (Type w)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op ⋙ ℱ.val) T} (h : x.Compatible),
(x.functorPushforward G).Compatible$$$
Lean4
/-- `CompatiblePreserving` functors indeed preserve compatible families. -/
theorem functorPushforward : (x.functorPushforward G).Compatible :=
by
rintro Z₁ Z₂ W g₁ g₂ f₁' f₂' H₁ H₂ eq
unfold FamilyOfElements.functorPushforward
rcases getFunctorPushforwardStructure H₁ with ⟨X₁, f₁, h₁, hf₁, rfl⟩
rcases getFunctorPushforwardStructure H₂ with ⟨X₂, f₂, h₂, hf₂, rfl⟩
suffices ℱ.val.map (g₁ ≫ h₁).op (x f₁ hf₁) = ℱ.val.map (g₂ ≫ h₂).op (x f₂ hf₂) by simpa using this
apply hG.compatible ℱ h _ _ hf₁ hf₂
simpa using eq
