EtaleCohomology.exists_sectionEquality_open
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits TopologicalSpace Opposite
namespace EtaleCohomology
variable {A : Type (u + 1)} [Category.{u} A]
{FA : A → A → Type u} {CA : A → Type u}
[∀ M N, FunLike (FA M N) (CA M) (CA N)] [ConcreteCategory.{u} A FA]Lean source · full declaration
theorem exists_sectionEquality_open
{Y : Scheme.{u}} [Y.smallEtaleTopology.HasSheafCompose (forget A)]
(F : Sheaf Y.smallEtaleTopology A)
(U : Y.Etale) (a b : ToType (F.obj.obj (op U))) :
∃ W : U.left.Opens,
(∀ (V : Y.Etale) (g : V ⟶ U), F.obj.map g.op a = F.obj.map g.op b →
Set.range g.left ⊆ (W : Set U.left)) ∧
F.obj.map (MorphismProperty.Over.homMk
(P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤) W.ι rfl :
(Scheme.Etale.mk (W.ι ≫ U.hom) : Y.Etale) ⟶ U).op a =
F.obj.map (MorphismProperty.Over.homMk
(P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤) W.ι rfl :
(Scheme.Etale.mk (W.ι ≫ U.hom) : Y.Etale) ⟶ U).op b := by
let I := Σ V : Y.Etale, {g : V ⟶ U // F.obj.map g.op a = F.obj.map g.op b}
let image (i : I) : U.left.Opens :=
⟨Set.range i.2.val.left, i.2.val.left.isOpenMap.isOpen_range⟩
let W : U.left.Opens := ⨆ i : I, image i
let O : Y.Etale := Scheme.Etale.mk (W.ι ≫ U.hom)
let j : O ⟶ U := MorphismProperty.Over.homMk
(P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤) W.ι rfl
have hRange (i : I) : Set.range i.2.val.left ⊆ Set.range W.ι := by
rw [Scheme.Opens.range_ι]
intro x hx
exact Opens.mem_iSup.mpr ⟨i, hx⟩
let l (i : I) : i.1.left ⟶ W.toScheme :=
IsOpenImmersion.lift W.ι i.2.val.left (hRange i)
have hl (i : I) : l i ≫ W.ι = i.2.val.left :=
IsOpenImmersion.lift_fac W.ι i.2.val.left (hRange i)
let k (i : I) : i.1 ⟶ O := MorphismProperty.Over.homMk
(P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤) (l i) (by
change l i ≫ (W.ι ≫ U.hom) = i.1.hom
rw [← Category.assoc, hl]
exact i.2.val.w)
have hkj (i : I) : k i ≫ j = i.2.val := by
apply MorphismProperty.Over.Hom.ext
exact hl i
have hCover : Sieve.ofArrows (fun i : I => i.1) k ∈ Y.smallEtaleTopology O := by
apply (Scheme.ofArrows_mem_smallEtaleTopology_iff k).mpr
apply Set.eq_univ_of_forall
intro x
obtain ⟨i, v, hv⟩ := Opens.mem_iSup.mp x.property
refine Set.mem_iUnion.mpr ⟨i, v, ?_⟩
apply Subtype.ext
exact ((Scheme.Hom.comp_apply (l i) W.ι v).symm.trans
(congrArg (fun f : i.1.left ⟶ U.left => f v) (hl i))).trans hv
refine ⟨W, ?_, ?_⟩
· intro V g hg x hx
exact Opens.mem_iSup.mpr ⟨⟨V, g, hg⟩, hx⟩
· change F.obj.map j.op a = F.obj.map j.op b
apply F.isSeparated O (Sieve.ofArrows (fun i : I => i.1) k) hCover
intro T m hm
obtain ⟨i, d, rfl⟩ := (Sieve.mem_ofArrows_iff (fun i : I => i.1) k m).mp hm
have hi : F.obj.map (k i).op (F.obj.map j.op a) =
F.obj.map (k i).op (F.obj.map j.op b) := by
rw [← F.obj.map_comp_apply, ← F.obj.map_comp_apply, ← op_comp, hkj]
exact i.2.property
rw [op_comp, F.obj.map_comp_apply, F.obj.map_comp_apply, hi]