Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
feat(topology/sheaves/*): Notation for restriction of sections. (#16088)


Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
  • Loading branch information
erdOne and erdOne committed Oct 27, 2022
1 parent 9340cc9 commit 06c75af
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 0 deletions.
1 change: 1 addition & 0 deletions src/algebraic_geometry/Scheme.lean
Expand Up @@ -221,6 +221,7 @@ lemma basic_open_res_eq (i : op U ⟶ op V) [is_iso i] :
X.basic_open (X.presheaf.map i f) = X.basic_open f :=
RingedSpace.basic_open_res_eq _ i f

@[sheaf_restrict]
lemma basic_open_le : X.basic_open f ≤ U :=
RingedSpace.basic_open_le _ _

Expand Down
65 changes: 65 additions & 0 deletions src/topology/sheaves/presheaf.lean
Expand Up @@ -44,6 +44,71 @@ variables {C}

namespace presheaf

local attribute [instance] concrete_category.has_coe_to_sort concrete_category.has_coe_to_fun

/-- Tag lemmas to use in `Top.presheaf.restrict_tac`. -/
@[user_attribute]
meta def restrict_attr : user_attribute (tactic unit → tactic unit) unit :=
{ name := `sheaf_restrict,
descr := "tag lemmas to use in `Top.presheaf.restrict_tac`",
cache_cfg :=
{ mk_cache := λ ns, pure $ λ t, do
{ ctx <- tactic.local_context,
ctx.any_of (tactic.focus1 ∘ (tactic.apply' >=> (λ _, tactic.done)) >=> (λ _, t)) <|>
ns.any_of (tactic.focus1 ∘ (tactic.resolve_name >=> tactic.to_expr >=> tactic.apply' >=>
(λ _, tactic.done)) >=> (λ _, t)) },
dependencies := [] } }

/-- A tactic to discharge goals of type `U ≤ V` for `Top.presheaf.restrict_open` -/
meta def restrict_tac : Π (n : ℕ), tactic unit
| 0 := tactic.fail "`restrict_tac` failed"
| (n + 1) := monad.join (restrict_attr.get_cache <*> pure tactic.done) <|>
`[apply' le_trans, mjoin (restrict_attr.get_cache <*> pure (restrict_tac n))]

/-- A tactic to discharge goals of type `U ≤ V` for `Top.presheaf.restrict_open`.
Defaults to three iterations. -/
meta def restrict_tac' := restrict_tac 3

attribute [sheaf_restrict] bot_le le_top le_refl inf_le_left inf_le_right le_sup_left le_sup_right

example {X : Top} {v w x y z : opens X} (h₀ : v ≤ x) (h₁ : x ≤ z ⊓ w) (h₂ : x ≤ y ⊓ z) :
v ≤ y := by restrict_tac'

/-- The restriction of a section along an inclusion of open sets.
For `x : F.obj (op V)`, we provide the notation `x |_ₕ i` (`h` stands for `hom`) for `i : U ⟶ V`,
and the notation `x |_ₗ U ⟪i⟫` (`l` stands for `le`) for `i : U ≤ V`.
-/
def restrict {X : Top} {C : Type*} [category C] [concrete_category C]
{F : X.presheaf C} {V : opens X} (x : F.obj (op V)) {U : opens X} (h : U ⟶ V) : F.obj (op U) :=
F.map h.op x

localized "infixl ` |_ₕ `: 80 := Top.presheaf.restrict" in algebraic_geometry

localized "notation x ` |_ₗ `: 80 U ` ⟪` e `⟫ ` :=
@Top.presheaf.restrict _ _ _ _ _ _ x U (@hom_of_le (opens _) _ U _ e)" in algebraic_geometry

/-- The restriction of a section along an inclusion of open sets.
For `x : F.obj (op V)`, we provide the notation `x |_ U`, where the proof `U ≤ V` is inferred by
the tactic `Top.presheaf.restrict_tac'` -/
abbreviation restrict_open {X : Top} {C : Type*} [category C] [concrete_category C]
{F : X.presheaf C} {V : opens X} (x : F.obj (op V)) (U : opens X)
(e : U ≤ V . Top.presheaf.restrict_tac') : F.obj (op U) :=
x |_ₗ U ⟪e⟫

localized "infixl ` |_ `: 80 := Top.presheaf.restrict_open" in algebraic_geometry

@[simp]
lemma restrict_restrict {X : Top} {C : Type*} [category C] [concrete_category C]
{F : X.presheaf C} {U V W : opens X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : F.obj (op W)) :
x |_ V |_ U = x |_ U :=
by { delta restrict_open restrict, rw [← comp_apply, ← functor.map_comp], refl }

@[simp]
lemma map_restrict {X : Top} {C : Type*} [category C] [concrete_category C]
{F G : X.presheaf C} (e : F ⟶ G) {U V : opens X} (h : U ≤ V) (x : F.obj (op V)) :
e.app _ (x |_ U) = (e.app _ x) |_ U :=
by { delta restrict_open restrict, rw [← comp_apply, nat_trans.naturality, comp_apply] }

/-- Pushforward a presheaf on `X` along a continuous map `f : X ⟶ Y`, obtaining a presheaf
on `Y`. -/
def pushforward_obj {X Y : Top.{w}} (f : X ⟶ Y) (ℱ : X.presheaf C) : Y.presheaf C :=
Expand Down

0 comments on commit 06c75af

Please sign in to comment.