structure
L33 ↗IsSectional
AlgebraicGeometry.Scheme.TwoAffineOpenCover.IsSectional
A family of pairwise disjoint sections of c contained in the first affine open whose images form the complement of the second affine open.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicGeometry.Scheme.TwoAffineOpenCover
open CategoryTheory CategoryTheory.Limits Opposite
variable {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of
R))Lean source · full declaration
structure IsSectional {ι : Type v} (σ : ι → (Spec (.of R) ⟶ X)) : Prop where
/-- Each `σ i` is a section of `c`. -/
comp_eq : ∀ i, σ i ≫ c = 𝟙 _
/-- The image of each section lies in the first affine open. -/
range_subset : ∀ i, Set.range (σ i).base ⊆ (𝒱.U0 : Set X)
/-- The section images cover exactly the complement of the second affine open. -/
compl_eq_iUnion : (𝒱.U1 : Set X)ᶜ = ⋃ i, Set.range (σ i).base
/-- The images of distinct sections are disjoint. -/
pairwise_disjoint : Pairwise fun i j => Disjoint (Set.range (σ i).base) (Set.range (σ j).base)