NYLL
Module

RelEffCartierDiv_isInvertible_I_of_supportedIn.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_I_of_supportedIn
3 declarations indexed from sourceView source ↗

Module documentation

Rel Eff Cartier Div is Invertible I of supported In

Imports12
Imported by27

Declarations

theorem

isIso_top_ι

L48 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I_of_supportedIn.DInvSupported.isIso_top_ι
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I_of_supportedIn
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
  AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
  AlgebraicGeometry.isClosedImmersion_graphOver
attribute [-simp] AlgebraicGeometry.graphOver_fst_assoc
  AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
  AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc AlgebraicGeometry.graphOver_fst
  AlgebraicGeometry.RelEffCartierDiv.ofPoint_I AlgebraicGeometry.graphOver_snd
  AlgebraicGeometry.graphOver_snd_assoc
universe u
namespace DInvSupported
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
Lean source · statement
theorem isIso_top_ι (S : Scheme.{u}) : IsIso (⊤ : S.Opens).ι
theorem

main

L52 ↗
AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I_of_supportedIn.DInvSupported.main
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I_of_supportedIn
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
  AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
  AlgebraicGeometry.isClosedImmersion_graphOver
attribute [-simp] AlgebraicGeometry.graphOver_fst_assoc
  AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
  AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc AlgebraicGeometry.graphOver_fst
  AlgebraicGeometry.RelEffCartierDiv.ofPoint_I AlgebraicGeometry.graphOver_snd
  AlgebraicGeometry.graphOver_snd_assoc
universe u
namespace DInvSupported
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
Lean source · statement
theorem main
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] (U : 𝒞.Opens) [SmoothOfRelativeDimension 1 (U.ι
      ≫ f)]
    {r : ℕ} {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) (hD : D.SupportedIn U) :
    D.I.IsInvertible
theorem

isInvertible_I_of_supportedIn

L82 ↗
AlgebraicGeometry.RelEffCartierDiv.isInvertible_I_of_supportedIn
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isInvertible_I_of_supportedIn
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
  AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
  AlgebraicGeometry.isClosedImmersion_graphOver
attribute [-simp] AlgebraicGeometry.graphOver_fst_assoc
  AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
  AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc AlgebraicGeometry.graphOver_fst
  AlgebraicGeometry.RelEffCartierDiv.ofPoint_I AlgebraicGeometry.graphOver_snd
  AlgebraicGeometry.graphOver_snd_assoc
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isInvertible_I_of_supportedIn
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] (U : 𝒞.Opens) [SmoothOfRelativeDimension 1 (U.ι
      ≫ f)]
    {r : ℕ} {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) (hD : D.SupportedIn U) :
    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.