NYLL
Module

RelEffCartierDiv_isRepresentable_supportedIn.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isRepresentable_supportedIn
4 declarations indexed from sourceView source ↗

Module documentation

Representability of the presheaf of relative divisors supported in an open.

Imports8
Imported by3

Declarations

lemma

extendAlong_congr

L75 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isRepresentable_supportedIn.AlgebraicGeometry.RelEffCartierDiv.ChartRep.extendAlong_congr
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isRepresentable_supportedIn
attribute [-instance]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
  instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
attribute [-simp]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace ChartRep
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {r : ℕ} {V : S.Opens} {U : 𝒞.Opens}
  {hUV : U ≤ f ⁻¹ᵁ V}
Lean source · statement
lemma extendAlong_congr {T : Scheme.{u}} {gV₁ gV₂ : T ⟶ V} (hV : gV₁ = gV₂) {g : T ⟶ S}
    (hg₁ : gV₁ ≫ V.ι = g) (hg₂ : gV₂ ≫ V.ι = g)
    (D₁ : RelEffCartierDiv (f.resLE V U hUV) r gV₁) (D₂ : RelEffCartierDiv (f.resLE V U hUV) r gV₂)
    (hD : HEq D₁ D₂) :
    extendAlong f r V U hUV gV₁ g hg₁ D₁ = extendAlong f r V U hUV gV₂ g hg₂ D₂
lemma

extendAlong_heq

L83 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isRepresentable_supportedIn.AlgebraicGeometry.RelEffCartierDiv.ChartRep.extendAlong_heq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isRepresentable_supportedIn
attribute [-instance]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
  instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
attribute [-simp]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace ChartRep
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {r : ℕ} {V : S.Opens} {U : 𝒞.Opens}
  {hUV : U ≤ f ⁻¹ᵁ V}
Lean source · statement
lemma extendAlong_heq {T : Scheme.{u}} {gV₁ gV₂ : T ⟶ V} (hV : gV₁ = gV₂) {g₁ g₂ : T ⟶ S}
    (hg : g₁ = g₂) (hg₁ : gV₁ ≫ V.ι = g₁) (hg₂ : gV₂ ≫ V.ι = g₂)
    (D₁ : RelEffCartierDiv (f.resLE V U hUV) r gV₁) (D₂ : RelEffCartierDiv (f.resLE V U hUV) r gV₂)
    (hD : HEq D₁ D₂) :
    HEq (extendAlong f r V U hUV gV₁ g₁ hg₁ D₁) (extendAlong f r V U hUV gV₂ g₂ hg₂ D₂)
lemma

pullbackAlong_heq'

L91 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isRepresentable_supportedIn.AlgebraicGeometry.RelEffCartierDiv.ChartRep.pullbackAlong_heq'
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isRepresentable_supportedIn
attribute [-instance]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
  instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
attribute [-simp]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace ChartRep
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {r : ℕ} {V : S.Opens} {U : 𝒞.Opens}
  {hUV : U ≤ f ⁻¹ᵁ V}
omit [IsSeparated f] in
Lean source · statement
lemma pullbackAlong_heq' {T T' : Scheme.{u}} {y : T' ⟶ V} (D : RelEffCartierDiv (f.resLE V U
    hUV) r y)
    {φ₁ φ₂ : T ⟶ T'} (hφ : φ₁ = φ₂) {g₁ g₂ : T ⟶ V} (h₁ : φ₁ ≫ y = g₁) (h₂ : φ₂ ≫ y = g₂) :
    HEq (D.pullbackAlong φ₁ h₁) (D.pullbackAlong φ₂ h₂)
theorem

isRepresentable_supportedIn

L106 ↗
AlgebraicGeometry.RelEffCartierDiv.isRepresentable_supportedIn
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isRepresentable_supportedIn
attribute [-instance]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instNeg
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulInt
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAddCommGroup
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instAdd
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSub
  instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instSMulNat
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.instZero
attribute [-simp]
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app
universe u
open CategoryTheory CategoryTheory.Limits Opposite
open _root_.AlgebraicGeometry
    RelEffCartierDiv_isRepresentable_supportedIn.AlgebraicGeometry
      _root_.AlgebraicGeometry.RelEffCartierDiv
        RelEffCartierDiv_isRepresentable_supportedIn.AlgebraicGeometry.RelEffCartierDiv
    RelEffCartierDiv_isRepresentable_supportedIn.AlgebraicGeometry.RelEffCartierDiv.ChartRep in
Lean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isRepresentable_supportedIn
    {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) [IsSeparated f] [SmoothOfRelativeDimension 1 f] (r : ℕ)
    (V : S.affineOpens) (U : 𝒞.affineOpens) (hUV : (U : 𝒞.Opens) ≤ f ⁻¹ᵁ (V : S.Opens)) :
    ∃ X : Scheme.{u}, (0 < r → IsAffine X) ∧
      Nonempty ((RelEffCartierDiv.supportedIn f r U).toFunctor.RepresentableBy X)

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