Module

RelEffCartierDivFunctor.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivFunctor

21 declarations indexed from sourceView source ↗

Module documentation

Functoriality of relative effective Cartier divisors.

Imports1

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv

Imported by37

lemma

pullbackAlong_heq

L30 ↗

AlgebraicGeometry.RelEffCartierDiv.pullbackAlong_heq

Source context 6 commands

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

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

Lean source · statement

lemma pullbackAlong_heq {T T' : Scheme.{u}} {g' : T' ⟶ S} (D : RelEffCartierDiv f r g')
    (φ : T ⟶ T') {g₁ g₂ : T ⟶ S} (h₁ : φ ≫ g' = g₁) (h₂ : φ ≫ g' = g₂) :
    HEq (D.pullbackAlong φ h₁) (D.pullbackAlong φ h₂)

def

functor

L37 ↗

AlgebraicGeometry.RelEffCartierDiv.functor

Documentation

The presheaf assigning relative effective Cartier divisors to schemes over the base.

Source context 6 commands

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

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

Lean source · full declaration

def functor : Scheme.{u}ᵒᵖ ⥤ Type u where
  obj T := Σ g : unop T ⟶ S, RelEffCartierDiv f r g
  map φ := TypeCat.ofHom fun D => ⟨φ.unop ≫ D.1, D.2.pullbackAlong φ.unop rfl⟩
  map_id T := by
    refine ConcreteCategory.hom_ext _ _ fun D => ?_
    obtain ⟨g, D⟩ := D
    change (⟨𝟙 _ ≫ g, D.pullbackAlong (𝟙 _) rfl⟩ : Σ g : unop T ⟶ S, RelEffCartierDiv f r g) =
      ⟨g, D⟩
    exact Sigma.ext (Category.id_comp g)
      ((D.pullbackAlong_heq (𝟙 _) rfl (Category.id_comp g)).trans (heq_of_eq D.pullbackAlong_id))
  map_comp {T T' T''} φ ψ := by
    refine ConcreteCategory.hom_ext _ _ fun D => ?_
    obtain ⟨g, D⟩ := D
    change (⟨(ψ.unop ≫ φ.unop) ≫ g, D.pullbackAlong (ψ.unop ≫ φ.unop) rfl⟩ :
        Σ g : unop T'' ⟶ S, RelEffCartierDiv f r g) =
      ⟨ψ.unop ≫ φ.unop ≫ g, (D.pullbackAlong φ.unop rfl).pullbackAlong ψ.unop rfl⟩
    exact Sigma.ext (Category.assoc _ _ _)
      ((D.pullbackAlong_heq (ψ.unop ≫ φ.unop) rfl (Category.assoc _ _ _)).trans
        (heq_of_eq (D.pullbackAlong_comp φ.unop rfl ψ.unop rfl).symm))

lemma

functor_map_fst

L57 ↗

AlgebraicGeometry.RelEffCartierDiv.functor_map_fst

Source context 6 commands

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

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

Lean source · statement

lemma functor_map_fst {T T' : Scheme.{u}ᵒᵖ} (φ : T ⟶ T') (D : (RelEffCartierDiv.functor
    f r).obj T) :
    ((RelEffCartierDiv.functor f r).map φ D).1 = φ.unop ≫ D.1

lemma

functor_map_snd

L61 ↗

AlgebraicGeometry.RelEffCartierDiv.functor_map_snd

Source context 6 commands

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

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

Lean source · statement

lemma functor_map_snd {T T' : Scheme.{u}ᵒᵖ} (φ : T ⟶ T') (D : (RelEffCartierDiv.functor f r).obj
    T) :
    ((RelEffCartierDiv.functor f r).map φ D).2 = D.2.pullbackAlong φ.unop rfl

lemma

functor_map_apply

L65 ↗

AlgebraicGeometry.RelEffCartierDiv.functor_map_apply

Source context 6 commands

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

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

Lean source · statement

lemma functor_map_apply {T T' : Scheme.{u}ᵒᵖ} (φ : T ⟶ T')
    (D : (RelEffCartierDiv.functor f r).obj T) :
    (RelEffCartierDiv.functor f r).map φ D = ⟨φ.unop ≫ D.1, D.2.pullbackAlong φ.unop rfl⟩

def

IsUniversal

L72 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal

Documentation

The unique pullback property of a universal relative effective Cartier divisor.

Source context 7 commands

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

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

Lean source · statement

def IsUniversal {Y : Scheme.{u}} {y : Y ⟶ S} (Duniv : RelEffCartierDiv f r y) : Prop

def

lift

L83 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.lift

Documentation

The unique classifying morphism supplied by the universal pullback property.

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

def IsUniversal.lift (hU : Duniv.IsUniversal) {T : Scheme.{u}} {g : T ⟶ S}
    (D : RelEffCartierDiv f r g) : T ⟶ Y

lemma

lift_comp

L87 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.lift_comp

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.lift_comp (hU : Duniv.IsUniversal) {T : Scheme.{u}} {g : T ⟶ S}
    (D : RelEffCartierDiv f r g) : hU.lift D ≫ y = g

lemma

pullsBackOver_lift

L91 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.pullsBackOver_lift

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.pullsBackOver_lift (hU : Duniv.IsUniversal) {T : Scheme.{u}} {g : T ⟶ S}
    (D : RelEffCartierDiv f r g) : PullsBackOver Duniv (hU.lift D) (hU.lift_comp D) D

lemma

pullbackAlong_lift

L95 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.pullbackAlong_lift

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.pullbackAlong_lift (hU : Duniv.IsUniversal) {T : Scheme.{u}} {g : T ⟶ S}
    (D : RelEffCartierDiv f r g) : Duniv.pullbackAlong (hU.lift D) (hU.lift_comp D) = D

lemma

eq_lift

L99 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.eq_lift

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.eq_lift (hU : Duniv.IsUniversal) {T : Scheme.{u}} {g : T ⟶ S}
    {D : RelEffCartierDiv f r g} {φ : T ⟶ Y} (hφ : φ ≫ y = g) (h : PullsBackOver Duniv φ hφ D) :
    φ = hU.lift D

lemma

lift_pullbackAlong

L104 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.lift_pullbackAlong

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.lift_pullbackAlong (hU : Duniv.IsUniversal) {T : Scheme.{u}}
    (φ : T ⟶ Y) : hU.lift (Duniv.pullbackAlong φ rfl) = φ

lemma

hom_ext

L108 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.hom_ext

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.hom_ext (hU : Duniv.IsUniversal) {T : Scheme.{u}} {φ ψ : T ⟶ Y}
    (hy : φ ≫ y = ψ ≫ y)
    (h : Duniv.I.comap (mapOnProdOver f φ rfl) = Duniv.I.comap (mapOnProdOver f ψ hy.symm)) :
    φ = ψ

theorem

of_iso

L115 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.of_iso

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

theorem IsUniversal.of_iso {Y'' : Scheme.{u}} {y'' : Y'' ⟶ S} (hU : Duniv.IsUniversal) (e : Y'' ≅ Y)
    (he : e.hom ≫ y = y'') : (Duniv.pullbackAlong e.hom he).IsUniversal

def

homEquiv

L142 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.homEquiv

Documentation

The equivalence between classifying morphisms and relative effective Cartier divisors.

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · full declaration

def IsUniversal.homEquiv (hU : Duniv.IsUniversal) (T : Scheme.{u}) :
    (T ⟶ Y) ≃ Σ g : T ⟶ S, RelEffCartierDiv f r g where
  toFun φ := ⟨φ ≫ y, Duniv.pullbackAlong φ rfl⟩
  invFun D := hU.lift D.2
  left_inv φ := hU.lift_pullbackAlong φ
  right_inv D := Sigma.ext (hU.lift_comp D.2)
    ((Duniv.pullbackAlong_heq _ rfl (hU.lift_comp D.2)).trans (heq_of_eq (hU.pullbackAlong_lift
      D.2)))

lemma

homEquiv_apply

L151 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.homEquiv_apply

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.homEquiv_apply (hU : Duniv.IsUniversal) {T : Scheme.{u}} (φ : T ⟶ Y) :
    hU.homEquiv T φ = ⟨φ ≫ y, Duniv.pullbackAlong φ rfl⟩

lemma

homEquiv_symm_apply

L154 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.homEquiv_symm_apply

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.homEquiv_symm_apply (hU : Duniv.IsUniversal) {T : Scheme.{u}}
    (D : Σ g : T ⟶ S, RelEffCartierDiv f r g) : (hU.homEquiv T).symm D = hU.lift D.2

def

representableBy

L158 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.representableBy

Documentation

The representation of the relative divisor presheaf supplied by a universal divisor.

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · full declaration

def IsUniversal.representableBy (hU : Duniv.IsUniversal) :
    (RelEffCartierDiv.functor f r).RepresentableBy Y where
  homEquiv {T} := hU.homEquiv T
  homEquiv_comp {T T'} φ ψ := by
    change (⟨(φ ≫ ψ) ≫ y, Duniv.pullbackAlong (φ ≫ ψ) rfl⟩ : Σ g : T ⟶ S, RelEffCartierDiv f r g) =
      ⟨φ ≫ ψ ≫ y, (Duniv.pullbackAlong ψ rfl).pullbackAlong φ rfl⟩
    exact Sigma.ext (Category.assoc _ _ _)
      ((Duniv.pullbackAlong_heq (φ ≫ ψ) rfl (Category.assoc _ _ _)).trans
        (heq_of_eq (Duniv.pullbackAlong_comp ψ rfl φ rfl).symm))

lemma

representableBy_homEquiv_apply

L168 ↗

AlgebraicGeometry.RelEffCartierDiv.IsUniversal.representableBy_homEquiv_apply

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

lemma IsUniversal.representableBy_homEquiv_apply (hU : Duniv.IsUniversal) {T : Scheme.{u}}
    (φ : T ⟶ Y) :
    hU.representableBy.homEquiv φ = ⟨φ ≫ y, Duniv.pullbackAlong φ rfl⟩

theorem

isUniversal_of_representableBy

L172 ↗

AlgebraicGeometry.RelEffCartierDiv.isUniversal_of_representableBy

Source context 10 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}

Lean source · statement

theorem isUniversal_of_representableBy (e : (RelEffCartierDiv.functor f r).RepresentableBy Y) :
    (e.homEquiv (𝟙 Y)).2.IsUniversal

theorem

isRepresentable_functor_iff

L200 ↗

AlgebraicGeometry.RelEffCartierDiv.isRepresentable_functor_iff

Source context 11 commands

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

open CategoryTheory CategoryTheory.Limits Opposite
universe u
namespace AlgebraicGeometry
namespace RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ)
variable {f r} in
variable {f r}
section Representability
variable {Y : Scheme.{u}} {y : Y ⟶ S}
variable {Duniv : RelEffCartierDiv f r y}
variable (f r) in

Lean source · statement

theorem isRepresentable_functor_iff :
    (RelEffCartierDiv.functor f r).IsRepresentable ↔
      ∃ (Y : Scheme.{u}) (y : Y ⟶ S) (Duniv : RelEffCartierDiv f r y), Duniv.IsUniversal

Module documentation

Declarations