Module

DirectedCover.lean

Nyll.SchemeTheory.WeilRestriction.DirectedCover

7 declarations indexed from sourceView source ↗

Module documentation

A locally directed refinement of an open cover

Given an open cover of a scheme, consider every open subset contained in the image of some member of that cover. These open subsets form a basis, and their inclusion ordering makes the associated open cover locally directed. A chosen containing member supplies a refinement map to the original cover.

Imports5

Mathlib.AlgebraicGeometry.Cover.Directed
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Restrict
Mathlib.Topology.Sets.Opens

Imported by2

def

subordinateOpenCover

L40 ↗

SchemeTheory.WeilRestriction.subordinateOpenCover

Documentation

The open cover consisting of all open subsets contained in the image of a member of 𝒰.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X)

Lean source · full declaration

def subordinateOpenCover : Scheme.OpenCover.{u} X where
  I₀ := {V : X.Opens // ∃ i : 𝒰.I₀, V ≤ (𝒰.f i).opensRange}
  X V := V.1
  f V := V.1.ι
  mem₀ := by
    rw [Scheme.presieve₀_mem_precoverage_iff]
    refine ⟨?_, ?_⟩
    · intro x
      refine ⟨⟨(𝒰.f (𝒰.idx x)).opensRange, ⟨𝒰.idx x, le_rfl⟩⟩, ?_⟩
      change x ∈ Set.range (𝒰.f (𝒰.idx x)).opensRange.ι
      rw [Scheme.Opens.range_ι]
      exact 𝒰.covers x
    · intro V
      exact inferInstanceAs (IsOpenImmersion V.1.ι)

instance

subordinateOpenCoverPreorder

L55 ↗

SchemeTheory.WeilRestriction.subordinateOpenCoverPreorder

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X)

Lean source · statement

instance subordinateOpenCoverPreorder : Preorder (subordinateOpenCover 𝒰).I₀

lemma

subordinateOpenCover_isBasis

L59 ↗

SchemeTheory.WeilRestriction.subordinateOpenCover_isBasis

Documentation

The members of the subordinate cover form a basis for the topology.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X)

Lean source · full declaration

lemma subordinateOpenCover_isBasis :
    TopologicalSpace.Opens.IsBasis
      (Set.range fun i : (subordinateOpenCover 𝒰).I₀ ↦
        ((subordinateOpenCover 𝒰).f i).opensRange) := by
  rw [TopologicalSpace.Opens.isBasis_iff_nbhd]
  intro V x hx
  let W : X.Opens := V ⊓ (𝒰.f (𝒰.idx x)).opensRange
  let j : (subordinateOpenCover 𝒰).I₀ := ⟨W, ⟨𝒰.idx x, inf_le_right⟩⟩
  refine ⟨W, ⟨j, ?_⟩, ?_, inf_le_left⟩
  · exact Scheme.Opens.opensRange_ι W
  · exact ⟨hx, 𝒰.covers x⟩

instance

subordinateOpenCoverLocallyDirected

L71 ↗

SchemeTheory.WeilRestriction.subordinateOpenCoverLocallyDirected

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X)

Lean source · statement

instance subordinateOpenCoverLocallyDirected :
    (subordinateOpenCover 𝒰).LocallyDirected

def

subordinateOpenCoverRefinementIndex

L80 ↗

SchemeTheory.WeilRestriction.subordinateOpenCoverRefinementIndex

Documentation

Choose a member of 𝒰 containing a given subordinate open subset.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X)

Lean source · statement

def subordinateOpenCoverRefinementIndex (i : (subordinateOpenCover 𝒰).I₀) : 𝒰.I₀

def

subordinateOpenCoverRefinementMap

L85 ↗

SchemeTheory.WeilRestriction.subordinateOpenCoverRefinementMap

Documentation

The map from a subordinate open subset to its chosen containing member of the original cover.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X)

Lean source · statement

def subordinateOpenCoverRefinementMap (i : (subordinateOpenCover 𝒰).I₀) :
    (subordinateOpenCover 𝒰).X i ⟶ 𝒰.X (subordinateOpenCoverRefinementIndex 𝒰 i)

lemma

subordinateOpenCoverRefinementMap_comp

L96 ↗

SchemeTheory.WeilRestriction.subordinateOpenCoverRefinementMap_comp

Documentation

The refinement maps commute with the structure maps to the base.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
open CategoryTheory AlgebraicGeometry
noncomputable section
universe u v
namespace SchemeTheory.WeilRestriction
variable {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X)

Lean source · statement

lemma subordinateOpenCoverRefinementMap_comp (i : (subordinateOpenCover 𝒰).I₀) :
    subordinateOpenCoverRefinementMap 𝒰 i ≫
        𝒰.f (subordinateOpenCoverRefinementIndex 𝒰 i) =
      (subordinateOpenCover 𝒰).f i

Module documentation

A locally directed refinement of an open cover

Declarations

subordinateOpenCover

subordinateOpenCoverPreorder

subordinateOpenCover_isBasis

subordinateOpenCoverLocallyDirected

subordinateOpenCoverRefinementIndex

subordinateOpenCoverRefinementMap

subordinateOpenCoverRefinementMap_comp