NYLL
Module

RelEffCartierDivRestrict.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivRestrict
21 declarations indexed from sourceView source ↗

Module documentation

Restriction of relative effective Cartier divisors to opens.

Imports3
Imported by13

Declarations

def

resProdMap

L35 ↗
AlgebraicGeometry.RelEffCartierDiv.resProdMap
Documentation

The natural open-immersion map from the restricted fiber product to the original fiber product.

Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
def resProdMap : pullback (f.resLE V U hUV) gV ⟶ pullback f g
instance

isOpenImmersion_resProdMap

L38 ↗
AlgebraicGeometry.RelEffCartierDiv.isOpenImmersion_resProdMap
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
instance isOpenImmersion_resProdMap : IsOpenImmersion (resProdMap f V U hUV gV g hg)
lemma

resProdMap_fst

L41 ↗
AlgebraicGeometry.RelEffCartierDiv.resProdMap_fst
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
lemma resProdMap_fst : resProdMap f V U hUV gV g hg ≫ pullback.fst f g = pullback.fst _ _ ≫ U.ι
lemma

resProdMap_snd

L45 ↗
AlgebraicGeometry.RelEffCartierDiv.resProdMap_snd
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
lemma resProdMap_snd : resProdMap f V U hUV gV g hg ≫ pullback.snd f g = pullback.snd _ _
lemma

isPullback_of_comp_mono

L48 ↗
AlgebraicGeometry.RelEffCartierDiv.isPullback_of_comp_mono
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
lemma isPullback_of_comp_mono {A B W Z : Scheme.{u}} (a : A ⟶ W) (b : B ⟶ W) (i : W ⟶ Z) [Mono i]
    {a' : A ⟶ Z} {b' : B ⟶ Z} (ha : a ≫ i = a') (hb : b ≫ i = b') :
    IsPullback (pullback.fst a b) (pullback.snd a b) a' b'
lemma

isPullback_resProdMap

L54 ↗
AlgebraicGeometry.RelEffCartierDiv.isPullback_resProdMap
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
lemma isPullback_resProdMap :
    IsPullback (resProdMap f V U hUV gV g hg) (pullback.fst (f.resLE V U hUV) gV)
      (pullback.fst f g) U.ι
lemma

range_resProdMap

L76 ↗
AlgebraicGeometry.RelEffCartierDiv.range_resProdMap
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd2
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
lemma range_resProdMap :
    Set.range (resProdMap f V U hUV gV g hg) = (pullback.fst f g) ⁻¹' (U : Set 𝒞)
lemma

range_resProdMap'

L83 ↗
AlgebraicGeometry.RelEffCartierDiv.range_resProdMap'
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
section ResProd2
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S) (hg : gV ≫ V.ι = g)
Lean source · statement
lemma range_resProdMap' :
    Set.range (resProdMap f V U hUV gV g hg) = ((pullback.fst f g) ⁻¹ᵁ U : (pullback f g).Opens)
lemma

isIso_pullback_snd_resProdMap

L96 ↗
AlgebraicGeometry.RelEffCartierDiv.isIso_pullback_snd_resProdMap
Source context 8 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Restrict
variable (hg : gV ≫ V.ι = g) (D : RelEffCartierDiv f r g) (hD : D.SupportedIn U)
include hD in
Lean source · statement
lemma isIso_pullback_snd_resProdMap :
    IsIso (pullback.snd (resProdMap f V U hUV gV g hg) D.I.subschemeι)
def

restrictAlong

L110 ↗
AlgebraicGeometry.RelEffCartierDiv.restrictAlong
Documentation

Restrict a relative effective Cartier divisor supported in U along the indicated open subsets of the curve and base.

Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Restrict
variable (hg : gV ≫ V.ι = g) (D : RelEffCartierDiv f r g) (hD : D.SupportedIn U)
Lean source · statement
def restrictAlong : RelEffCartierDiv (f.resLE V U hUV) r gV
lemma

restrictAlong_I

L130 ↗
AlgebraicGeometry.RelEffCartierDiv.restrictAlong_I
Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Restrict
variable (hg : gV ≫ V.ι = g) (D : RelEffCartierDiv f r g) (hD : D.SupportedIn U)
Lean source · statement
lemma restrictAlong_I :
    (restrictAlong f r V U hUV gV g hg D hD).I = D.I.comap (resProdMap f V U hUV gV g hg)
instance

isClosedImmersion_subschemeι_resProdMap

L139 ↗
AlgebraicGeometry.RelEffCartierDiv.isClosedImmersion_subschemeι_resProdMap
Source context 7 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Extend
variable (hg : gV ≫ V.ι = g) (D' : RelEffCartierDiv (f.resLE V U hUV) r gV)
Lean source · statement
instance isClosedImmersion_subschemeι_resProdMap [IsSeparated f] :
    IsClosedImmersion (D'.I.subschemeι ≫ resProdMap f V U hUV gV g hg)
def

extendAlong

L152 ↗
AlgebraicGeometry.RelEffCartierDiv.extendAlong
Documentation

Extend a relative effective Cartier divisor from the restricted curve using the ideal of its image in the original fiber product.

Source context 8 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Extend
variable (hg : gV ≫ V.ι = g) (D' : RelEffCartierDiv (f.resLE V U hUV) r gV)
variable [IsSeparated f]
Lean source · statement
def extendAlong : RelEffCartierDiv f r g
lemma

extendAlong_I

L169 ↗
AlgebraicGeometry.RelEffCartierDiv.extendAlong_I
Source context 8 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Extend
variable (hg : gV ≫ V.ι = g) (D' : RelEffCartierDiv (f.resLE V U hUV) r gV)
variable [IsSeparated f]
Lean source · statement
lemma extendAlong_I :
    (extendAlong f r V U hUV gV g hg D').I = (D'.I.subschemeι ≫ resProdMap f V U hUV gV g
      hg).ker
lemma

extendAlong_I_eq_map

L173 ↗
AlgebraicGeometry.RelEffCartierDiv.extendAlong_I_eq_map
Source context 8 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Extend
variable (hg : gV ≫ V.ι = g) (D' : RelEffCartierDiv (f.resLE V U hUV) r gV)
variable [IsSeparated f]
Lean source · statement
lemma extendAlong_I_eq_map :
    (extendAlong f r V U hUV gV g hg D').I = D'.I.map (resProdMap f V U hUV gV g hg)
lemma

extendAlong_supportedIn

L176 ↗
AlgebraicGeometry.RelEffCartierDiv.extendAlong_supportedIn
Source context 8 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
variable {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Extend
variable (hg : gV ≫ V.ι = g) (D' : RelEffCartierDiv (f.resLE V U hUV) r gV)
variable [IsSeparated f]
Lean source · statement
lemma extendAlong_supportedIn : (extendAlong f r V U hUV gV g hg D').SupportedIn U
lemma

extendAlong_restrictAlong

L201 ↗
AlgebraicGeometry.RelEffCartierDiv.extendAlong_restrictAlong
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
  {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section RoundTrip
variable [IsSeparated f] (hg : gV ≫ V.ι = g)
Lean source · statement
lemma extendAlong_restrictAlong (D : RelEffCartierDiv f r g) (hD : D.SupportedIn U) :
    extendAlong f r V U hUV gV g hg (restrictAlong f r V U hUV gV g hg D hD) = D
lemma

restrictAlong_extendAlong

L209 ↗
AlgebraicGeometry.RelEffCartierDiv.restrictAlong_extendAlong
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
  {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section RoundTrip
variable [IsSeparated f] (hg : gV ≫ V.ι = g)
Lean source · statement
lemma restrictAlong_extendAlong (D' : RelEffCartierDiv (f.resLE V U hUV) r gV) :
    restrictAlong f r V U hUV gV g hg (extendAlong f r V U hUV gV g hg D')
      (extendAlong_supportedIn f r V U hUV gV g hg D') = D'
lemma

isPullback_mapOnProdOver_resProdMap

L232 ↗
AlgebraicGeometry.RelEffCartierDiv.isPullback_mapOnProdOver_resProdMap
Source context 5 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
  {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Naturality
Lean source · statement
lemma isPullback_mapOnProdOver_resProdMap {T₁ T₂ : Scheme.{u}} {gV₁ : T₁ ⟶ V} {gV₂ : T₂ ⟶ V}
    {g₁ : T₁ ⟶ S} {g₂ : T₂ ⟶ S} (hg₁ : gV₁ ≫ V.ι = g₁) (hg₂ : gV₂ ≫ V.ι = g₂)
    (φ : T₁ ⟶ T₂) (hφV : φ ≫ gV₂ = gV₁) (hφ : φ ≫ g₂ = g₁) :
    IsPullback (mapOnProdOver (f.resLE V U hUV) φ hφV) (resProdMap f V U hUV gV₁ g₁ hg₁)
      (resProdMap f V U hUV gV₂ g₂ hg₂) (mapOnProdOver f φ hφ)
lemma

extendAlong_pullbackAlong

L245 ↗
AlgebraicGeometry.RelEffCartierDiv.extendAlong_pullbackAlong
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
  {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Naturality
variable [IsSeparated f] in
Lean source · statement
lemma extendAlong_pullbackAlong {T₁ T₂ : Scheme.{u}} {gV₁ : T₁ ⟶ V} {gV₂ : T₂ ⟶ V}
    {g₁ : T₁ ⟶ S} {g₂ : T₂ ⟶ S} (hg₁ : gV₁ ≫ V.ι = g₁) (hg₂ : gV₂ ≫ V.ι = g₂)
    (D' : RelEffCartierDiv (f.resLE V U hUV) r gV₂) (φ : T₁ ⟶ T₂) (hφV : φ ≫ gV₂ = gV₁)
    (hφ : φ ≫ g₂ = g₁) :
    extendAlong f r V U hUV gV₁ g₁ hg₁ (D'.pullbackAlong φ hφV) =
      (extendAlong f r V U hUV gV₂ g₂ hg₂ D').pullbackAlong φ hφ
lemma

range_subset_of_supportedIn

L271 ↗
AlgebraicGeometry.RelEffCartierDiv.range_subset_of_supportedIn
Source context 6 commands

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

open CategoryTheory CategoryTheory.Limits
universe u
namespace AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (V : S.Opens) (U : 𝒞.Opens) (hUV : U ≤ f ⁻¹ᵁ V)
  {T : Scheme.{u}} (gV : T ⟶ V) (g : T ⟶ S)
section Range
include hUV in
Lean source · statement
lemma range_subset_of_supportedIn {g : T ⟶ S} (D : RelEffCartierDiv f r g)
    (hD : D.SupportedIn U) (hr : 0 < r) : Set.range g ⊆ Set.range V.ι

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.