English
If P1 ≃ P2 via a natural equivalence, and P1 is a sheaf for R, then P2 is a sheaf for R, with additional structure.
Русский
Если P1 ≃ P2 через естественную эквивалентность, и P1 — sheaf для R, тогда P2 — тоже sheaf для R.
LaTeX
$$isSheafFor_of_nat_equiv (e) (he) {X} {R} (hP1) : IsSheafFor P2 R$$
Lean4
/-- If `P₁ : Cᵒᵖ ⥤ Type w` and `P₂ : Cᵒᵖ ⥤ Type w` are two naturally equivalent
presheaves, and `P₁` is a sheaf for a presieve `R`, then `P₂` is also a sheaf for `R`. -/
theorem isSheafFor_of_nat_equiv {P₁ : Cᵒᵖ ⥤ Type w} {P₂ : Cᵒᵖ ⥤ Type w'} (e : ∀ ⦃X : C⦄, P₁.obj (op X) ≃ P₂.obj (op X))
(he : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)), e (P₁.map f.op x) = P₂.map f.op (e x)) {X : C} {R : Presieve X}
(hP₁ : IsSheafFor P₁ R) : IsSheafFor P₂ R := fun x₂ hx₂ ↦
by
have he' : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)), e.symm (P₂.map f.op x) = P₁.map f.op (e.symm x) :=
fun X Y f x ↦ e.injective (by simp only [Equiv.apply_symm_apply, he])
let x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
have hx₁ : x₁.Compatible := fun Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ fac ↦
e.injective (by simp only [he, Equiv.apply_symm_apply, hx₂ g₁ g₂ h₁ h₂ fac, x₁])
have : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂) := fun t₂ ↦ by
simp only [FamilyOfElements.IsAmalgamation, x₁, ← he', EmbeddingLike.apply_eq_iff_eq]
refine ⟨e (hP₁.amalgamate x₁ hx₁), ?_, ?_⟩
· dsimp
simp only [this, Equiv.symm_apply_apply]
exact IsSheafFor.isAmalgamation hP₁ hx₁
· intro t₂ ht₂
refine e.symm.injective ?_
simp only [Equiv.symm_apply_apply]
exact hP₁.isSeparatedFor x₁ _ _ (by simpa only [this] using ht₂) (IsSheafFor.isAmalgamation hP₁ hx₁)
