EtaleCohomology.exists_global_lift_of_mono_of_local_lifts
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomologyLean source · full declaration
theorem exists_global_lift_of_mono_of_local_lifts
{T : TopCat.{u}}
{F G : TopCat.Sheaf (Type u) T}
(m : F ⟶ G) [Mono m] (t : G.obj.obj (op (⊤ : Opens T)))
(hlift : ∀ x : T, ∃ U : Opens T, x ∈ U ∧
∃ a : F.obj.obj (op U), m.hom.app (op U) a =
G.obj.map (homOfLE (show U ≤ ⊤ from le_top)).op t) :
∃ a : F.obj.obj (op (⊤ : Opens T)), m.hom.app (op ⊤) a = t := by
classical
choose U hx a ha using hlift
let FP : T.Presheaf (Type u) := F.obj
let GP : T.Presheaf (Type u) := G.obj
let j : ∀ x : T, U x ⟶ (⊤ : Opens T) := fun _ => homOfLE le_top
have hcover : (⊤ : Opens T) ≤ iSup U := by
intro x _
exact Opens.mem_iSup.mpr ⟨x, hx x⟩
have hmP : Mono m.hom := (TopCat.Sheaf.forget (Type u) T).map_mono m
have hmU (W : Opens T) : Mono (m.hom.app (op W)) :=
(NatTrans.mono_iff_mono_app m.hom).mp hmP (op W)
have hcompat : TopCat.Presheaf.IsCompatible FP U a := by
intro x y
apply (CategoryTheory.mono_iff_injective (m.hom.app (op (U x ⊓ U y)))).mp
(hmU (U x ⊓ U y))
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply,
m.hom.naturality, m.hom.naturality, ConcreteCategory.comp_apply,
ConcreteCategory.comp_apply, ha x, ha y]
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply,
← GP.map_comp, ← GP.map_comp]
rfl
obtain ⟨s, hs, _⟩ := TopCat.Sheaf.existsUnique_gluing' F U ⊤ j hcover a hcompat
refine ⟨s, ?_⟩
apply TopCat.Sheaf.eq_of_locally_eq' G U ⊤ j hcover
intro x
rw [← ConcreteCategory.comp_apply, ← m.hom.naturality,
ConcreteCategory.comp_apply, hs x]
exact ha x