Module

RelEffCartierDiv_exists_I_eq_mul.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_mul

76 declarations indexed from sourceView source ↗

Module documentation

Factoring a relative divisor ideal

Factors the defining ideal of a relative divisor as a product after a suitable base change.

Imports13

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.ZariskisMainTheorem
Mathlib.Algebra.Module.LocalizedModule.Exact
Mathlib.Algebra.Module.LocalizedModule.Submodule
Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.Flat.EquationalCriterion
Mathlib.RingTheory.Ideal.Colon
Mathlib.RingTheory.Ideal.Maps
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isInvertible_I
Nyll.AlgebraicCurves.Foundations.Algebra.Module_rankAtStalk_eq_of_forall_localizedModule_equiv
Nyll.AlgebraicCurves.Foundations.Algebra.Module_finitePresentation_of_rankAtStalk_eq
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv

Imported by8

theorem

eq_span_singleton_mul_colon

L58 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.eq_span_singleton_mul_colon

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

theorem eq_span_singleton_mul_colon (K : Ideal B) (t : B) (h : K ≤ span {t}) :
    K = span {t} * K.colon {t}

theorem

colon_span_singleton_mul

L66 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.colon_span_singleton_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

theorem colon_span_singleton_mul {t : B} (ht : t ∈ nonZeroDivisors B) (J : Ideal B) :
    (span {t} * J).colon {t} = J

theorem

mul_mem_span_singleton_mul_iff

L79 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.mul_mem_span_singleton_mul_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

theorem mul_mem_span_singleton_mul_iff {t : B} (ht : t ∈ nonZeroDivisors B) (J : Ideal B)
    (y : B) : y * t ∈ span {t} * J ↔ y ∈ J

theorem

ker_mkQ_comp_toSpanSingleton

L90 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.ker_mkQ_comp_toSpanSingleton

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

theorem ker_mkQ_comp_toSpanSingleton (K : Ideal B) (t : B) :
    LinearMap.ker (K.mkQ ∘ₗ LinearMap.toSpanSingleton B B t) = K.colon {t}

theorem

range_mkQ_comp_toSpanSingleton

L96 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.range_mkQ_comp_toSpanSingleton

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

theorem range_mkQ_comp_toSpanSingleton (K : Ideal B) (t : B) :
    LinearMap.range (K.mkQ ∘ₗ LinearMap.toSpanSingleton B B t) =
      Submodule.map K.mkQ (Ideal.span {t})

def

quotColonEquivMapSpan

L102 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.quotColonEquivMapSpan

Documentation

Multiplication by t identifies the quotient by the colon ideal with the image of its span.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

def quotColonEquivMapSpan (K : Ideal B) (t : B) :
    (B ⧸ K.colon {t}) ≃ₗ[B] ↥(Submodule.map K.mkQ (Ideal.span {t}))

def

quotEquivMapSpanOfMul

L110 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.quotEquivMapSpanOfMul

Documentation

For a nonzero divisor t, the quotient by J identifies with the image of its span modulo span {t} * J.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

def quotEquivMapSpanOfMul {t : B} (ht : t ∈ nonZeroDivisors B) (J : Ideal B) :
    (B ⧸ J) ≃ₗ[B] ↥(Submodule.map (span {t} * J).mkQ (Ideal.span {t}))

theorem

quotEquivMapSpanOfMul_apply_mk

L115 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.quotEquivMapSpanOfMul_apply_mk

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

theorem quotEquivMapSpanOfMul_apply_mk {t : B} (ht : t ∈ nonZeroDivisors B)
    (J : Ideal B) (x : B) :
    ((quotEquivMapSpanOfMul ht J (Ideal.Quotient.mk J x) : ↥(Submodule.map (span {t} * J).mkQ
      (Ideal.span {t}))) : B ⧸ span {t} * J) = Ideal.Quotient.mk (span {t} * J) (x * t)

theorem

map_mkQ_eq_ker_factor

L121 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.map_mkQ_eq_ker_factor

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section colon
variable {B : Type*} [CommRing B]
open _root_.Ideal

Lean source · statement

theorem map_mkQ_eq_ker_factor {K I : Ideal B} (h : K ≤ I) :
    Submodule.map K.mkQ I =
      (RingHom.ker (Ideal.Quotient.factor h)).restrictScalars B

theorem

nonempty_linearEquiv_ker_prod

L143 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.nonempty_linearEquiv_ker_prod

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section split
variable {R : Type*} [CommRing R] {M P : Type*} [AddCommGroup M] [Module R M]
  [AddCommGroup P] [Module R P]

Lean source · statement

theorem nonempty_linearEquiv_ker_prod [Module.Projective R P] (f : M →ₗ[R] P)
    (hf : Function.Surjective f) : Nonempty (M ≃ₗ[R] (LinearMap.ker f × P))

theorem

projective_of_projective_ker

L162 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.projective_of_projective_ker

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section split
variable {R : Type*} [CommRing R] {M P : Type*} [AddCommGroup M] [Module R M]
  [AddCommGroup P] [Module R P]

Lean source · statement

theorem projective_of_projective_ker [Module.Projective R P] (f : M →ₗ[R] P)
    (hf : Function.Surjective f) [Module.Projective R (LinearMap.ker f)] :
    Module.Projective R M

theorem

flat_ker

L168 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_ker

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section split
variable {R : Type*} [CommRing R] {M P : Type*} [AddCommGroup M] [Module R M]
  [AddCommGroup P] [Module R P]

Lean source · statement

theorem flat_ker [Module.Projective R P] [Module.Flat R M] (f : M →ₗ[R] P)
    (hf : Function.Surjective f) : Module.Flat R (LinearMap.ker f)

theorem

finite_ker

L174 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finite_ker

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section split
variable {R : Type*} [CommRing R] {M P : Type*} [AddCommGroup M] [Module R M]
  [AddCommGroup P] [Module R P]

Lean source · statement

theorem finite_ker [Module.Projective R P] [Module.Finite R M] (f : M →ₗ[R] P)
    (hf : Function.Surjective f) : Module.Finite R (LinearMap.ker f)

theorem

rankAtStalk_eq_ker_add

L180 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.rankAtStalk_eq_ker_add

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section split
variable {R : Type*} [CommRing R] {M P : Type*} [AddCommGroup M] [Module R M]
  [AddCommGroup P] [Module R P]

Lean source · statement

theorem rankAtStalk_eq_ker_add [Module.Projective R P] [Module.Finite R M] [Module.Flat R M]
    [Module.Finite R P] (f : M →ₗ[R] P) (hf : Function.Surjective f) :
    Module.rankAtStalk (R := R) M = Module.rankAtStalk (LinearMap.ker f) + Module.rankAtStalk P

theorem

projective_of_finitePresentation_of_flat

L193 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.projective_of_finitePresentation_of_flat

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section projective

Lean source · statement

theorem projective_of_finitePresentation_of_flat {R : Type*} [CommRing R] (P : Type*)
    [AddCommGroup P] [Module R P] [Module.Flat R P] [Module.FinitePresentation R P] :
    Module.Projective R P

theorem

isClosedImmersion_inclusion

L204 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.isClosedImmersion_inclusion

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme

Lean source · statement

theorem isClosedImmersion_inclusion {X : Scheme.{u}} {I J : X.IdealSheafData} (h : I ≤ J) :
    IsClosedImmersion (Scheme.IdealSheafData.inclusion h)

theorem

flat_localizedModule_of_flat

L211 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_localizedModule_of_flat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem flat_localizedModule_of_flat {R₀ A : Type v} [CommRing R₀] [CommRing A] [Algebra R₀ A]
    (p : Submonoid A)
    {M : Type v} [AddCommGroup M] [Module R₀ M] [Module A M] [IsScalarTower R₀ A M]
    [Module.Flat R₀ M] : Module.Flat R₀ (LocalizedModule p M)

theorem

hom_predicate_seam

L231 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.hom_predicate_seam

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem hom_predicate_seam {Z Y : Scheme.{u}} (q : Z ⟶ Y) (U : Y.Opens)
    (P : ∀ {R S : CommRingCat.{u}}, (R ⟶ S) → Prop) :
    P ((q ∣_ U).appTop) ↔ P (q.appLE U (q ⁻¹ᵁ U) le_rfl)

theorem

mk_subschemeObjIso_inclusion_appLE

L241 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.mk_subschemeObjIso_inclusion_appLE

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · full declaration

theorem mk_subschemeObjIso_inclusion_appLE {X : Scheme.{u}} {I J : X.IdealSheafData}
    (h : I ≤ J) (W : X.affineOpens) :
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal W)) ≫ ((I.subschemeObjIso W).inv ≫
      ((Scheme.IdealSheafData.inclusion h).app (I.subschemeι ⁻¹ᵁ W.1) ≫
        J.subscheme.presheaf.map (eqToHom (by
          rw [← Scheme.IdealSheafData.inclusion_subschemeι h]; rfl :
            J.subschemeι ⁻¹ᵁ W.1 =
              Scheme.IdealSheafData.inclusion h ⁻¹ᵁ (I.subschemeι ⁻¹ᵁ W.1))).op) ≫
      (J.subschemeObjIso W).hom) =
    CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal W)) := by
  have h1 := Scheme.Hom.congr_app (Scheme.IdealSheafData.inclusion_subschemeι h) W.1
  rw [Scheme.Hom.comp_app] at h1
  simp only [← Category.assoc]
  rw [← Scheme.IdealSheafData.subschemeι_app, h1]
  have hpre : J.subschemeι ⁻¹ᵁ W.1 =
      Scheme.IdealSheafData.inclusion h ⁻¹ᵁ (I.subschemeι ⁻¹ᵁ W.1) := by
    rw [← Scheme.IdealSheafData.inclusion_subschemeι h]
    rfl
  change ((J.subschemeι.app W.1 ≫ J.subscheme.presheaf.map (eqToHom hpre.symm).op) ≫
    J.subscheme.presheaf.map (eqToHom hpre).op) ≫ (J.subschemeObjIso W).hom = _
  simp only [Category.assoc, ← Functor.map_comp, ← op_comp, eqToHom_trans,
    eqToHom_refl, op_id]
  erw [CategoryTheory.Functor.map_id]
  simp only [Category.id_comp, Scheme.IdealSheafData.subschemeι_app,
    Category.assoc, Iso.inv_hom_id, Category.comp_id]

theorem

presheaf_map_injective_of_eq

L267 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.presheaf_map_injective_of_eq

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem presheaf_map_injective_of_eq {X : Scheme.{u}} {U V : X.Opens} (hUV : U = V)
    (i : Opposite.op V ⟶ Opposite.op U) : Function.Injective (X.presheaf.map i).hom

theorem

inclusion_app_mk_eq_zero_iff

L275 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.inclusion_app_mk_eq_zero_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem inclusion_app_mk_eq_zero_iff {X : Scheme.{u}} {I J : X.IdealSheafData} (h : I ≤ J)
    (W : X.affineOpens) (y : Γ(X, W.1)) :
    ((Scheme.IdealSheafData.inclusion h).app (I.subschemeι ⁻¹ᵁ W.1)).hom
        ((I.subschemeObjIso W).inv.hom (Ideal.Quotient.mk (I.ideal W) y)) = 0 ↔
      y ∈ J.ideal W

theorem

subschemeObjIso_inv_mk_surjective

L296 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.subschemeObjIso_inv_mk_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · full declaration

theorem subschemeObjIso_inv_mk_surjective {X : Scheme.{u}} (I : X.IdealSheafData)
    (W : X.affineOpens) :
    Function.Surjective fun y : Γ(X, W.1) =>
      (I.subschemeObjIso W).inv.hom (Ideal.Quotient.mk (I.ideal W) y) :=
  (ConcreteCategory.bijective_of_isIso (I.subschemeObjIso W).inv).2.comp
    Ideal.Quotient.mk_surjective

theorem

forall_finrank_eq_iff_of_isAffine

L303 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.forall_finrank_eq_iff_of_isAffine

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem forall_finrank_eq_iff_of_isAffine {X Y : Scheme.{u}} [IsAffine X] [IsAffine Y]
    (g : X ⟶ Y) [Flat g] [IsFinite g] (n : ℕ) :
    (∀ y : Y, g.finrank y = n) ↔
      ∀ x : PrimeSpectrum Γ(Y, ⊤), g.appTop.hom.finrank x = n

theorem

forall_mem_finrank_eq_iff

L320 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.forall_mem_finrank_eq_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem forall_mem_finrank_eq_iff {Z Y : Scheme.{u}} (q : Z ⟶ Y) [Flat q] [IsFinite q]
    (U : Y.affineOpens) (n : ℕ) :
    (∀ s ∈ U.1, q.finrank s = n) ↔
      ∀ x : PrimeSpectrum Γ(Y, U.1), (q.appLE U.1 (q ⁻¹ᵁ U.1) le_rfl).hom.finrank x = n

theorem

mul_le_fst

L337 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.mul_le_fst

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem mul_le_fst {X : Scheme.{u}} (I J : X.IdealSheafData) : I * J ≤ I

theorem

mul_le_snd

L341 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.mul_le_snd

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem mul_le_snd {X : Scheme.{u}} (I J : X.IdealSheafData) : I * J ≤ J

theorem

map_mem_nonZeroDivisors_basicOpen

L345 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.map_mem_nonZeroDivisors_basicOpen

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section generic
open _root_.AlgebraicGeometry.Scheme
universe v in

Lean source · statement

theorem map_mem_nonZeroDivisors_basicOpen {X : Scheme.{u}} (V : X.affineOpens) (f : Γ(X, V.1))
    {g : Γ(X, V.1)} (hg : g ∈ nonZeroDivisors Γ(X, V.1)) :
    (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom g ∈
      nonZeroDivisors Γ(X, X.basicOpen f)

theorem

exists_affineOpen_eq_span_nonZeroDivisor

L362 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.exists_affineOpen_eq_span_nonZeroDivisor

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}

Lean source · statement

theorem exists_affineOpen_eq_span_nonZeroDivisor {r : ℕ} (D : RelEffCartierDiv c r t)
    (x : ↥(pullback c t)) :
    ∃ U : (pullback c t).affineOpens, x ∈ U.1 ∧
      ∃ g ∈ nonZeroDivisors Γ(pullback c t, U.1), D.I.ideal U = Ideal.span {g}

theorem

exists_affineOpen_le_span_nonZeroDivisor

L369 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.exists_affineOpen_le_span_nonZeroDivisor

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}

Lean source · statement

theorem exists_affineOpen_le_span_nonZeroDivisor {r : ℕ} (D : RelEffCartierDiv c r t)
    {V₀ : TopologicalSpace.Opens ↥(pullback c t)} {x : ↥(pullback c t)} (hx : x ∈ V₀) :
    ∃ W : (pullback c t).affineOpens, x ∈ W.1 ∧ W.1 ≤ V₀ ∧
      ∃ g ∈ nonZeroDivisors Γ(pullback c t, W.1),
        D.I.ideal W = Ideal.span {g}

theorem

isFinite_mul

L406 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.isFinite_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}

Lean source · statement

theorem isFinite_mul {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) :
    IsFinite ((D.I * E.I).subschemeι ≫ pullback.snd c t)

instance

algRA

L503 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.algRA

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance algRA : Algebra Rᵤ Aᵤ

instance

algAJ

L507 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.algAJ

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance algAJ : Algebra Aᵤ AJᵤ

instance

algRJ

L511 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.algRJ

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance algRJ : Algebra Rᵤ AJᵤ

instance

towerRAJ

L516 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.towerRAJ

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance towerRAJ : IsScalarTower Rᵤ Aᵤ AJᵤ

instance

isFinite_subschemeι_comp_snd

L528 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.isFinite_subschemeι_comp_snd

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance isFinite_subschemeι_comp_snd : IsFinite ((D.I * E.I).subschemeι ≫ pullback.snd c
  t)

instance

algRI

L531 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.algRI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance algRI : Algebra Rᵤ AIᵤ

theorem

finite_A

L535 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finite_A

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem finite_A : Module.Finite Rᵤ Aᵤ

theorem

inclusion_comp_eq_subschemeι_J

L542 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.inclusion_comp_eq_subschemeι_J

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem inclusion_comp_eq_subschemeι_J :
    Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫ ((D.I * E.I).subschemeι ≫
      pullback.snd c t) =
      E.I.subschemeι ≫ pullback.snd c t

instance

isFinite_inclusion_comp_J

L548 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.isFinite_inclusion_comp_J

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance isFinite_inclusion_comp_J :
    IsFinite (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫ ((D.I * E.I).subschemeι ≫
      pullback.snd c t))

instance

flat_inclusion_comp_J

L554 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_inclusion_comp_J

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance flat_inclusion_comp_J :
    Flat (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫ ((D.I * E.I).subschemeι ≫
      pullback.snd c t))

theorem

finite_AJ

L561 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finite_AJ

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem finite_AJ : Module.Finite Rᵤ AJᵤ

theorem

flat_AJ

L569 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_AJ

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem flat_AJ : Module.Flat Rᵤ AJᵤ

theorem

rankAtStalk_AJ

L585 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.rankAtStalk_AJ

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem rankAtStalk_AJ (x : PrimeSpectrum Rᵤ) : Module.rankAtStalk (R := Rᵤ) AJᵤ x = s

theorem

inclusion_comp_eq_subschemeι_I

L593 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.inclusion_comp_eq_subschemeι_I

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem inclusion_comp_eq_subschemeι_I :
    Scheme.IdealSheafData.inclusion (mul_le_fst D.I E.I) ≫ ((D.I * E.I).subschemeι ≫
      pullback.snd c t) =
      D.I.subschemeι ≫ pullback.snd c t

instance

isFinite_inclusion_comp_I

L599 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.isFinite_inclusion_comp_I

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance isFinite_inclusion_comp_I :
    IsFinite (Scheme.IdealSheafData.inclusion (mul_le_fst D.I E.I) ≫ ((D.I * E.I).subschemeι ≫
      pullback.snd c t))

instance

flat_inclusion_comp_I

L605 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_inclusion_comp_I

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

instance flat_inclusion_comp_I :
    Flat (Scheme.IdealSheafData.inclusion (mul_le_fst D.I E.I) ≫ ((D.I * E.I).subschemeι ≫
      pullback.snd c t))

theorem

finite_AI

L612 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finite_AI

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem finite_AI : Module.Finite Rᵤ AIᵤ

theorem

flat_AI

L618 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_AI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem flat_AI : Module.Flat Rᵤ AIᵤ

theorem

rankAtStalk_AI

L634 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.rankAtStalk_AI

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem rankAtStalk_AI (x : PrimeSpectrum Rᵤ) : Module.rankAtStalk (R := Rᵤ) AIᵤ x = r

theorem

finitePresentation_AI

L641 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finitePresentation_AI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem finitePresentation_AI : Module.FinitePresentation Rᵤ AIᵤ

theorem

projective_AI

L646 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.projective_AI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem projective_AI : Module.Projective Rᵤ AIᵤ

theorem

inclusion_app_comp_algebraMap

L652 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.inclusion_app_comp_algebraMap

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem inclusion_app_comp_algebraMap :
    ((Scheme.IdealSheafData.inclusion (mul_le_fst D.I E.I)).app
        (((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)).hom.comp (algebraMap Rᵤ Aᵤ) =
      algebraMap Rᵤ AIᵤ

def

πI

L662 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.πI

Documentation

The section algebra map induced by the inclusion of the subscheme of D into that of D * E.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

def πI : Aᵤ →ₐ[Rᵤ] AIᵤ

theorem

πI_surjective

L673 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.πI_surjective

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem πI_surjective : Function.Surjective (πI D E U)

def

kerπIEquiv

L680 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.kerπIEquiv

Documentation

The ring-homomorphism kernel and linear-map kernel of the inclusion on sections have the same underlying module.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

def kerπIEquiv : (RingHom.ker (πI D E U).toRingHom) ≃ₗ[Rᵤ]
    ↥(LinearMap.ker (πI D E U).toLinearMap)

theorem

finite_kerπI

L689 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finite_kerπI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem finite_kerπI : Module.Finite Rᵤ (RingHom.ker (πI D E U).toRingHom)

instance

residualBasicOpenAlgebra

L698 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.residualBasicOpenAlgebra

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
section localizedChart

Lean source · statement

instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
    Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))

instance

divisorBasicOpenAlgebra

L711 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.divisorBasicOpenAlgebra

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
    Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((E.I.subscheme.presheaf.map (homOfLE
    (E.I.subscheme.basicOpen_le _)).op).hom).toAlgebra

Lean source · statement

instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ((D.I * E.I).subscheme,
  ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ((D.I * E.I).subscheme, (D.I * E.I).subscheme.basicOpen h)

instance

residualBasicOpenAlgebraOverDivisor

L717 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.residualBasicOpenAlgebraOverDivisor

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
    Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((E.I.subscheme.presheaf.map (homOfLE
    (E.I.subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ((D.I * E.I).subscheme,
  ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ((D.I * E.I).subscheme, (D.I * E.I).subscheme.basicOpen h) :=
  (((D.I * E.I).subscheme.presheaf.map (homOfLE
    ((D.I * E.I).subscheme.basicOpen_le h)).op).hom).toAlgebra

Lean source · statement

instance residualBasicOpenAlgebraOverDivisor (h : Aᵤ) : Algebra Γ((D.I *
  E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))

instance

divisorBasicOpenIsLocalization

L739 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.divisorBasicOpenIsLocalization

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
    Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((E.I.subscheme.presheaf.map (homOfLE
    (E.I.subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ((D.I * E.I).subscheme,
  ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ((D.I * E.I).subscheme, (D.I * E.I).subscheme.basicOpen h) :=
  (((D.I * E.I).subscheme.presheaf.map (homOfLE
    ((D.I * E.I).subscheme.basicOpen_le h)).op).hom).toAlgebra
noncomputable local instance residualBasicOpenAlgebraOverDivisor (h : Aᵤ) : Algebra Γ((D.I *
  E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((algebraMap Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))).comp
    (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1))).toAlgebra

Lean source · statement

instance divisorBasicOpenIsLocalization (h : Aᵤ) : IsLocalization.Away h Γ((D.I *
  E.I).subscheme, (D.I * E.I).subscheme.basicOpen h)

theorem

basicOpen_sections_equiv_kernel

L743 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.basicOpen_sections_equiv_kernel

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
    Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((E.I.subscheme.presheaf.map (homOfLE
    (E.I.subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ((D.I * E.I).subscheme,
  ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ((D.I * E.I).subscheme, (D.I * E.I).subscheme.basicOpen h) :=
  (((D.I * E.I).subscheme.presheaf.map (homOfLE
    ((D.I * E.I).subscheme.basicOpen_le h)).op).hom).toAlgebra
noncomputable local instance residualBasicOpenAlgebraOverDivisor (h : Aᵤ) : Algebra Γ((D.I *
  E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((algebraMap Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))).comp
    (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1))).toAlgebra
local instance divisorBasicOpenIsLocalization (h : Aᵤ) : IsLocalization.Away h Γ((D.I *
  E.I).subscheme, (D.I * E.I).subscheme.basicOpen h) :=
  (U.2.preimage ((D.I * E.I).subschemeι ≫ pullback.snd c t)).isLocalization_basicOpen h

Lean source · statement

theorem basicOpen_sections_equiv_kernel
    (W : (pullback c t).affineOpens) (hWle : W.1 ≤ (pullback.snd c t) ⁻¹ᵁ U.1)
    (g : Γ(pullback c t, W.1)) (hgnzd : g ∈ nonZeroDivisors Γ(pullback c t, W.1))
    (hgspan : D.I.ideal W = Ideal.span {g})
    (h : Aᵤ) (hhle : (D.I * E.I).subscheme.basicOpen h ≤ (D.I * E.I).subschemeι ⁻¹ᵁ W.1) :
    Nonempty (Γ(E.I.subscheme,
          E.I.subscheme.basicOpen
            (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ
              U.1)
              Γ(E.I.subscheme,
                (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
                  ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) ≃ₗ[Γ((D.I *
                    E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)]
        ↥((RingHom.ker (πI D E U).toRingHom).localized'
          Γ((D.I * E.I).subscheme, (D.I * E.I).subscheme.basicOpen h) (Submonoid.powers h)
          (Algebra.linearMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c
            t) ⁻¹ᵁ U.1)
            Γ((D.I * E.I).subscheme, (D.I * E.I).subscheme.basicOpen h))))

theorem

localizedModule_equiv_of_chart

L991 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.localizedModule_equiv_of_chart

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
    Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((E.I.subscheme.presheaf.map (homOfLE
    (E.I.subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ((D.I * E.I).subscheme,
  ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ((D.I * E.I).subscheme, (D.I * E.I).subscheme.basicOpen h) :=
  (((D.I * E.I).subscheme.presheaf.map (homOfLE
    ((D.I * E.I).subscheme.basicOpen_le h)).op).hom).toAlgebra
noncomputable local instance residualBasicOpenAlgebraOverDivisor (h : Aᵤ) : Algebra Γ((D.I *
  E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
    Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
  ((algebraMap Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ(E.I.subscheme,
      E.I.subscheme.basicOpen
        (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(E.I.subscheme,
            (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
              ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))).comp
    (algebraMap Γ((D.I * E.I).subscheme, ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ(E.I.subscheme,
      (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
        ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1))).toAlgebra
local instance divisorBasicOpenIsLocalization (h : Aᵤ) : IsLocalization.Away h Γ((D.I *
  E.I).subscheme, (D.I * E.I).subscheme.basicOpen h) :=
  (U.2.preimage ((D.I * E.I).subschemeι ≫ pullback.snd c t)).isLocalization_basicOpen h

Lean source · statement

theorem localizedModule_equiv_of_chart
    (W : (pullback c t).affineOpens) (hWle : W.1 ≤ (pullback.snd c t) ⁻¹ᵁ U.1)
    (g : Γ(pullback c t, W.1)) (hgnzd : g ∈ nonZeroDivisors Γ(pullback c t, W.1))
    (hgspan : D.I.ideal W = Ideal.span {g})
    (h : Aᵤ) (hhle : (D.I * E.I).subscheme.basicOpen h ≤ (D.I * E.I).subschemeι ⁻¹ᵁ W.1) :
    Nonempty (LocalizedModule (Submonoid.powers h)
      Γ(E.I.subscheme,
        (Scheme.IdealSheafData.inclusion (mul_le_snd D.I E.I) ≫
          ((D.I * E.I).subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) ≃ₗ[Γ((D.I * E.I).subscheme,
        ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)]
      LocalizedModule (Submonoid.powers h) (RingHom.ker (πI D E U).toRingHom))

theorem

exists_basicOpen_localizedModule_equiv

L1102 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.exists_basicOpen_localizedModule_equiv

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem exists_basicOpen_localizedModule_equiv (z : (D.I * E.I).subscheme)
    (hz : z ∈ ((D.I * E.I).subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1) :
    ∃ h : Aᵤ, z ∈ (D.I * E.I).subscheme.basicOpen h ∧
      Nonempty (LocalizedModule (Submonoid.powers h) AJᵤ ≃ₗ[Aᵤ]
        LocalizedModule (Submonoid.powers h) (RingHom.ker (πI D E U).toRingHom))

theorem

span_setOf_localizedModule_equiv_eq_top

L1117 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.span_setOf_localizedModule_equiv_eq_top

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem span_setOf_localizedModule_equiv_eq_top :
    Ideal.span {h : Aᵤ | Nonempty (LocalizedModule (Submonoid.powers h) AJᵤ ≃ₗ[Aᵤ]
      LocalizedModule (Submonoid.powers h) (RingHom.ker (πI D E U).toRingHom))} =
    ⊤

theorem

flat_kerπI

L1126 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_kerπI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem flat_kerπI : Module.Flat Rᵤ (RingHom.ker (πI D E U).toRingHom)

theorem

rankAtStalk_kerπI

L1135 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.rankAtStalk_kerπI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem rankAtStalk_kerπI (x : PrimeSpectrum Rᵤ) :
    Module.rankAtStalk (R := Rᵤ) (RingHom.ker (πI D E U).toRingHom) x = s

theorem

finitePresentation_kerπI

L1147 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finitePresentation_kerπI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem finitePresentation_kerπI :
    Module.FinitePresentation Rᵤ (RingHom.ker (πI D E U).toRingHom)

theorem

projective_kerπI

L1153 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.projective_kerπI

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem projective_kerπI : Module.Projective Rᵤ (RingHom.ker (πI D E U).toRingHom)

theorem

projective_A

L1158 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.projective_A

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem projective_A : Module.Projective Rᵤ Aᵤ

theorem

flat_A

L1165 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_A

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem flat_A : Module.Flat Rᵤ Aᵤ

theorem

rankAtStalk_A

L1169 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.rankAtStalk_A

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem rankAtStalk_A (x : PrimeSpectrum Rᵤ) : Module.rankAtStalk (R := Rᵤ) Aᵤ x = r + s

theorem

finitePresentation_A

L1179 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finitePresentation_A

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section chartModules
variable {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (U : T.affineOpens)
local notation "Rᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace (T)))))
  (Opposite.op (Subtype.val U))
local notation "Aᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D * RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t))))) (Subtype.val U)))
local notation "AJᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I E))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_snd (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))
local notation "AIᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (RelEffCartierDiv.I D))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (mul_le_fst (RelEffCartierDiv.I D)
        (RelEffCartierDiv.I E)) ≫ (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D *
        RelEffCartierDiv.I E) ≫ pullback.snd c t)))))) (Subtype.val U)))

Lean source · statement

theorem finitePresentation_A : Module.FinitePresentation Rᵤ Aᵤ

theorem

flat_mul

L1186 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.flat_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}

Lean source · statement

theorem flat_mul {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) :
    Flat ((D.I * E.I).subschemeι ≫ pullback.snd c t)

theorem

locallyOfFinitePresentation_mul

L1198 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.locallyOfFinitePresentation_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}

Lean source · statement

theorem locallyOfFinitePresentation_mul {r s : ℕ} (D : RelEffCartierDiv c r t)
    (E : RelEffCartierDiv c s t) :
    LocallyOfFinitePresentation ((D.I * E.I).subschemeι ≫ pullback.snd c t)

theorem

finrank_mul

L1216 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul.DivisorSum.finrank_mul

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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
namespace DivisorSum
section construction
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}

Lean source · statement

theorem finrank_mul {r s : ℕ} (D : RelEffCartierDiv c r t) (E : RelEffCartierDiv c s t) (y : T) :
    ((D.I * E.I).subschemeι ≫ pullback.snd c t).finrank y = r + s

theorem

exists_I_eq_mul

L1229 ↗

AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_mul

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_mul
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

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_mul
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] [SmoothOfRelativeDimension 1 f]
    {r s : ℕ} {T : Scheme.{u}} {g : T ⟶ S}
    (D : RelEffCartierDiv f r g) (E : RelEffCartierDiv f s g) :
    ∃ F : RelEffCartierDiv f (r + s) g, F.I = D.I * E.I

Module documentation

Factoring a relative divisor ideal

Declarations