NYLL
Module

RelEffCartierDiv_isInvertible_I.lean

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

Module documentation

Invertibility of relative divisor ideals

Shows local invertibility of the defining ideal of a relative effective Cartier divisor.

Imports9
Imported by52

Declarations

theorem

I_eq_top_of_degree_zero

L50 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I.AlgebraicGeometry.RelEffCartierDiv.CartierInduction.I_eq_top_of_degree_zero
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace CartierInduction
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] [SmoothOfRelativeDimension 1 f]
omit [IsSeparated f] [SmoothOfRelativeDimension 1 f] in
Lean source · statement
theorem I_eq_top_of_degree_zero {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f 0 g) :
    D.I = ⊤
theorem

step

L64 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I.AlgebraicGeometry.RelEffCartierDiv.CartierInduction.step
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace CartierInduction
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] [SmoothOfRelativeDimension 1 f]
Lean source · statement
theorem step (r : ℕ)
    (ih : ∀ {T : Scheme.{u}} {g : T ⟶ S} (E : RelEffCartierDiv f r g), E.I.IsInvertible)
    {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f (r + 1) g) : D.I.IsInvertible
theorem

isInvertible

L116 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I.AlgebraicGeometry.RelEffCartierDiv.CartierInduction.isInvertible
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace CartierInduction
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] [SmoothOfRelativeDimension 1 f]
Lean source · full declaration
theorem isInvertible : ∀ (r : ℕ) {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g),
    D.I.IsInvertible
  | 0, _, _, D => by
    rw [I_eq_top_of_degree_zero D]
    exact Scheme.IdealSheafData.isInvertible_top
  | r + 1, _, _, D => step r (fun E => isInvertible r E) D
theorem

isInvertible_I

L125 ↗
AlgebraicGeometry.RelEffCartierDiv.isInvertible_I
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isInvertible_I {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S}
  [IsSeparated f] [SmoothOfRelativeDimension 1 f]
    {r : ℕ} {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) : D.I.IsInvertible

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