English
If f is locally bijective and N is a sheaf, then precomposition with f induces a bijection between morphisms M₂ → N and M₁ → N.
Русский
Если f локально биективен, а N — каска, то предсоставление через f задаёт биекцию между морфизмами M₂ → N и M₁ → N.
LaTeX
$$$(M_2 \to N) \cong (M_1 \to N)$ via $\varphi \mapsto \varphi \circ f$$$
Lean4
/-- The bijection `(M₂ ⟶ N) ≃ (M₁ ⟶ N)` induced by a locally bijective morphism
`f : M₁ ⟶ M₂` of presheaves of modules, when `N` is a sheaf. -/
@[simps]
noncomputable def homEquivOfIsLocallyBijective : (M₂ ⟶ N) ≃ (M₁ ⟶ N)
where
toFun φ := f ≫ φ
invFun
ψ :=
homMk
(((J.W_of_isLocallyBijective ((PresheafOfModules.toPresheaf R).map f)).homEquiv _ hN).symm
((PresheafOfModules.toPresheaf R).map ψ))
(by
obtain ⟨φ, hφ⟩ :=
((J.W_of_isLocallyBijective ((PresheafOfModules.toPresheaf R).map f)).homEquiv _ hN).surjective
((PresheafOfModules.toPresheaf R).map ψ)
simp only [← hφ, Equiv.symm_apply_apply]
replace hφ : ∀ (Z : Cᵒᵖ) (x : M₁.obj Z), φ.app Z (f.app Z x) = ψ.app Z x := fun Z x ↦
CategoryTheory.congr_fun (congr_app hφ Z) x
intro X r y
apply hN.isSeparated _ _ (Presheaf.imageSieve_mem J ((toPresheaf R).map f) y)
rintro Y p ⟨x : M₁.obj _, hx : f.app _ x = M₂.map p.op y⟩
have hφ' : ∀ (z : M₂.obj X), φ.app _ (M₂.map p.op z) = N.map p.op (φ.app _ z) :=
CategoryTheory.congr_fun (φ.naturality p.op)
change N.map p.op (φ.app X (r • y)) = N.map p.op (r • φ.app X y)
rw [← hφ', M₂.map_smul, ← hx, ← (f.app _).hom.map_smul, hφ, (ψ.app _).hom.map_smul, ← hφ, hx, N.map_smul, hφ'])
left_inv
φ :=
(toPresheaf _).map_injective
(((J.W_of_isLocallyBijective ((PresheafOfModules.toPresheaf R).map f)).homEquiv _ hN).left_inv
((PresheafOfModules.toPresheaf R).map φ))
right_inv
ψ :=
(toPresheaf _).map_injective
(((J.W_of_isLocallyBijective ((PresheafOfModules.toPresheaf R).map f)).homEquiv _ hN).right_inv
((PresheafOfModules.toPresheaf R).map ψ))
