Module

RelEffCartierDiv_isUniversal_empty.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isUniversal_empty

2 declarations indexed from sourceView source ↗

Module documentation

The empty relative divisor is universal.

Imports2

Imported by3

theorem

isUniversal_empty_aux

L38 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isUniversal_empty.AlgebraicGeometry.RelEffCartierDiv.isUniversal_empty_aux

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isUniversal_empty
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry

Lean source · statement

theorem isUniversal_empty_aux {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) :
    (RelEffCartierDiv.empty f (𝟙 S)).IsUniversal

theorem

isUniversal_empty

L49 ↗

AlgebraicGeometry.RelEffCartierDiv.isUniversal_empty

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isUniversal_empty
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isUniversal_empty {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) :
    (RelEffCartierDiv.empty f (𝟙 S)).IsUniversal

Module documentation

Declarations

isUniversal_empty_aux

isUniversal_empty