Module

RelEffCartierDivSupportedIn.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSupportedIn

13 declarations indexed from sourceView source ↗

Module documentation

Relative effective Cartier divisors supported in a fixed open.

Imports4

Mathlib.CategoryTheory.Subfunctor.Basic
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.PullbackCarrier
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivFunctor

Imported by53

def

SupportedIn

L31 ↗

AlgebraicGeometry.RelEffCartierDiv.SupportedIn

Documentation

The divisor support lies over the chosen open subset of the curve.

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}

Lean source · statement

def SupportedIn {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) (U : 𝒞.Opens) : Prop

lemma

supportedIn_iff

L34 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedIn_iff

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}

Lean source · statement

lemma supportedIn_iff {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) (U : 𝒞.Opens) :
    D.SupportedIn U ↔ ∀ x ∈ D.I.support, pullback.fst f g x ∈ U

lemma

mono

L38 ↗

AlgebraicGeometry.RelEffCartierDiv.SupportedIn.mono

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}

Lean source · statement

lemma SupportedIn.mono {T : Scheme.{u}} {g : T ⟶ S} {D : RelEffCartierDiv f r g} {U U' : 𝒞.Opens}
    (h : D.SupportedIn U) (hUU' : U ≤ U') : D.SupportedIn U'

lemma

supportedIn_top

L42 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedIn_top

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}

Lean source · statement

lemma supportedIn_top {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) :
    D.SupportedIn ⊤

lemma

pullbackAlong

L46 ↗

AlgebraicGeometry.RelEffCartierDiv.SupportedIn.pullbackAlong

Source context 4 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}

Lean source · statement

lemma SupportedIn.pullbackAlong {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S}
    {D : RelEffCartierDiv f r g'} {U : 𝒞.Opens} (h : D.SupportedIn U) (φ : T ⟶ T')
    (hφ : φ ≫ g' = g) : (D.pullbackAlong φ hφ).SupportedIn U

def

supportedInLocus

L61 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedInLocus

Documentation

The open locus in the base whose divisor fibers are contained in the chosen open subset of the curve.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
section Locus
variable {T : Scheme.{u}} {g : T ⟶ S}

Lean source · full declaration

def supportedInLocus (D : RelEffCartierDiv f r g) (U : 𝒞.Opens) : T.Opens where
  carrier := {t | ∀ z : ↥D.I.subscheme, (D.I.subschemeι ≫ pullback.snd f g) z = t →
    pullback.fst f g (D.I.subschemeι z) ∈ U}
  is_open' := by
    have := D.isFinite
    have hcl : IsClosed ((D.I.subschemeι ≫ pullback.snd f g) ''
        ((D.I.subschemeι ≫ pullback.fst f g) ⁻¹ᵁ U : Set ↥D.I.subscheme)ᶜ) :=
      (D.I.subschemeι ≫ pullback.snd f g).isClosedMap _
        ((D.I.subschemeι ≫ pullback.fst f g) ⁻¹ᵁ U).2.isClosed_compl
    convert hcl.isOpen_compl using 1
    ext t
    simp only [Set.mem_ofPred_eq, Set.mem_compl_iff, Set.mem_image, not_exists, not_and]
    exact ⟨fun h z hz hzt => hz (by simpa [Scheme.Hom.comp_apply] using h z hzt),
      fun h z hzt => by
        by_contra hz
        exact h z (by simpa [Scheme.Hom.comp_apply] using hz) hzt⟩

lemma

mem_supportedInLocus_iff

L78 ↗

AlgebraicGeometry.RelEffCartierDiv.mem_supportedInLocus_iff

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
section Locus
variable {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

lemma mem_supportedInLocus_iff (D : RelEffCartierDiv f r g) (U : 𝒞.Opens) (t : T) :
    t ∈ D.supportedInLocus U ↔ ∀ z : ↥D.I.subscheme, (D.I.subschemeι ≫ pullback.snd f g) z = t →
      pullback.fst f g (D.I.subschemeι z) ∈ U

lemma

supportedIn_pullbackAlong_iff

L83 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedIn_pullbackAlong_iff

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
section Locus
variable {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

lemma supportedIn_pullbackAlong_iff (D : RelEffCartierDiv f r g) (U : 𝒞.Opens)
    {T' : Scheme.{u}} {g' : T' ⟶ S} (φ : T' ⟶ T) (hφ : φ ≫ g = g') :
    (D.pullbackAlong φ hφ).SupportedIn U ↔ Set.range φ ⊆ (D.supportedInLocus U : Set T)

lemma

supportedIn_iff_supportedInLocus_eq_top

L111 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedIn_iff_supportedInLocus_eq_top

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
section Locus
variable {T : Scheme.{u}} {g : T ⟶ S}

Lean source · statement

lemma supportedIn_iff_supportedInLocus_eq_top (D : RelEffCartierDiv f r g) (U : 𝒞.Opens) :
    D.SupportedIn U ↔ D.supportedInLocus U = ⊤

def

supportedIn

L126 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedIn

Documentation

The subfunctor of relative effective Cartier divisors whose supports lie over the chosen open subset of the curve.

Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
variable (f r)

Lean source · full declaration

def supportedIn (U : 𝒞.Opens) : Subfunctor (RelEffCartierDiv.functor f r) where
  obj T := {x | x.2.SupportedIn U}
  map {T T'} φ := by
    rintro ⟨g, D⟩ (hD : D.SupportedIn U)
    exact hD.pullbackAlong φ.unop rfl

lemma

mem_supportedIn_iff

L134 ↗

AlgebraicGeometry.RelEffCartierDiv.mem_supportedIn_iff

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
variable (f r)
variable {f r}

Lean source · statement

lemma mem_supportedIn_iff {U : 𝒞.Opens} {T : Scheme.{u}ᵒᵖ}
    (x : (RelEffCartierDiv.functor f r).obj T) :
    x ∈ (supportedIn f r U).obj T ↔ x.2.SupportedIn U

lemma

supportedIn_mono

L139 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedIn_mono

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
variable (f r)
variable {f r}

Lean source · statement

lemma supportedIn_mono {U U' : 𝒞.Opens} (h : U ≤ U') : supportedIn f r U ≤ supportedIn f r U'

lemma

supportedIn_top_eq

L142 ↗

AlgebraicGeometry.RelEffCartierDiv.supportedIn_top_eq

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ}
variable (f r)
variable {f r}

Lean source · statement

lemma supportedIn_top_eq : supportedIn f r (⊤ : 𝒞.Opens) = ⊤

Module documentation

Declarations