Module

RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul

74 declarations indexed from sourceView source ↗

Module documentation

Splitting a relative divisor along a section

Splits a relative divisor into the graph of a section and a residual divisor.

Imports8

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivOfPoint
Nyll.AlgebraicCurves.RelativeDivisors.Cartier
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.Algebra.Module.LocalizedModule.Exact
Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id
Nyll.AlgebraicCurves.Foundations.Algebra.Module_rankAtStalk_eq_of_forall_localizedModule_equiv
Nyll.AlgebraicCurves.Foundations.Algebra.Module_finitePresentation_of_rankAtStalk_eq

Imported by3

theorem

eq_span_singleton_mul_colon

L44 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.eq_span_singleton_mul_colon

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section ring
variable {R : Type*} [CommRing R]
open _root_.Ideal

Lean source · statement

theorem eq_span_singleton_mul_colon (I : Ideal R) (f : R) (h : I ≤ span {f}) :
    I = span {f} * I.colon {f}

theorem

span_singleton_mul_right_injective_of_mem

L52 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.span_singleton_mul_right_injective_of_mem

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section ring
variable {R : Type*} [CommRing R]
open _root_.Ideal

Lean source · statement

theorem span_singleton_mul_right_injective_of_mem {f : R} (hf : f ∈ nonZeroDivisors R)
    {J J' : Ideal R} (h : span {f} * J = span {f} * J') : J = J'

theorem

map_colon_of_finite

L64 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.map_colon_of_finite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section ring
variable {R : Type*} [CommRing R]
open _root_.Ideal

Lean source · statement

theorem map_colon_of_finite (M : Submonoid R) (S : Type*) [CommRing S] [Algebra R S]
    [IsLocalization M S] (I : Ideal R) {T : Set R} (hT : T.Finite) :
    (I.colon T).map (algebraMap R S) = (I.map (algebraMap R S)).colon (algebraMap R S '' T)

theorem

map_colon_span_of_finite

L88 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.map_colon_span_of_finite

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section ring
variable {R : Type*} [CommRing R]
open _root_.Ideal

Lean source · statement

theorem map_colon_span_of_finite (M : Submonoid R) (S : Type*) [CommRing S] [Algebra R S]
    [IsLocalization M S] (I : Ideal R) {T : Set R} (hT : T.Finite) :
    (I.colon (Ideal.span T)).map (algebraMap R S) =
      (I.map (algebraMap R S)).colon ((Ideal.span T).map (algebraMap R S))

theorem

ker_mkQ_comp_toSpanSingleton

L95 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.ker_mkQ_comp_toSpanSingleton

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section ring
variable {R : Type*} [CommRing R]
open _root_.Ideal

Lean source · statement

theorem ker_mkQ_comp_toSpanSingleton (I : Ideal R) (f : R) :
    LinearMap.ker (I.mkQ ∘ₗ LinearMap.toSpanSingleton R R f) = I.colon {f}

theorem

range_mkQ_comp_toSpanSingleton

L101 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.range_mkQ_comp_toSpanSingleton

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section ring
variable {R : Type*} [CommRing R]
open _root_.Ideal

Lean source · statement

theorem range_mkQ_comp_toSpanSingleton (I : Ideal R) (f : R) :
    LinearMap.range (I.mkQ ∘ₗ LinearMap.toSpanSingleton R R f) =
      Submodule.map I.mkQ (Ideal.span {f})

def

quotColonEquivMapSpan

L108 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.quotColonEquivMapSpan

Documentation

Multiplication by f identifies the quotient by the colon ideal with the image of (f) in R/I.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section ring
variable {R : Type*} [CommRing R]
open _root_.Ideal

Lean source · statement

def quotColonEquivMapSpan (I : Ideal R) (f : R) :
    (R ⧸ I.colon {f}) ≃ₗ[R] ↥(Submodule.map I.mkQ (Ideal.span {f}))

def

colonSheaf

L125 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.colonSheaf

Documentation

The ideal sheaf whose affine ideals are I : 𝔞, using finite generation to commute with localization.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section sheaf
variable {X : Scheme.{u}}
open _root_.AlgebraicGeometry.Scheme

Lean source · full declaration

def colonSheaf (I 𝔞 : X.IdealSheafData)
    (h𝔞 : ∀ U : X.affineOpens, (𝔞.ideal U).FG) : X.IdealSheafData where
  ideal U := (I.ideal U).colon (𝔞.ideal U)
  map_ideal_basicOpen U f := by
    obtain ⟨T, hT⟩ := h𝔞 U
    have := U.2.isLocalization_basicOpen f
    have key := map_colon_span_of_finite (Submonoid.powers f) Γ(X, X.basicOpen f)
      (I.ideal U) (T := (T : Set Γ(X, U.1))) T.finite_toSet
    rw [hT] at key
    have halg : algebraMap Γ(X, U.1) Γ(X, X.basicOpen f) =
        (X.presheaf.map (homOfLE <| X.basicOpen_le f).op).hom := rfl
    rw [halg] at key
    exact key.trans (congrArg₂ (fun (J K : Ideal Γ(X, X.basicOpen f)) => J.colon K)
      (I.map_ideal_basicOpen U f) (𝔞.map_ideal_basicOpen U f))

lemma

ideal_colonSheaf

L140 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.ideal_colonSheaf

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
section sheaf
variable {X : Scheme.{u}}
open _root_.AlgebraicGeometry.Scheme

Lean source · statement

lemma ideal_colonSheaf (I 𝔞 : X.IdealSheafData)
    (h𝔞 : ∀ U : X.affineOpens, (𝔞.ideal U).FG) (U : X.affineOpens) :
    (colonSheaf I 𝔞 h𝔞).ideal U = (I.ideal U).colon (𝔞.ideal U)

abbrev

graphHom

L157 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.graphHom

Documentation

The graph of a₀ in the fibre product over its fixed base morphism.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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

abbrev graphHom (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) : T ⟶ pullback c t

theorem

exists_affineOpen_ker_graph_eq_span_nonZeroDivisor

L160 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.exists_affineOpen_ker_graph_eq_span_nonZeroDivisor

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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_ker_graph_eq_span_nonZeroDivisor (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
    (x : ↥(pullback c t)) :
    ∃ U : (pullback c t).affineOpens, x ∈ U.1 ∧
      ∃ g ∈ nonZeroDivisors Γ(pullback c t, U.1), (graphHom a₀ h₀).ker.ideal U = Ideal.span {g}

theorem

fg_ideal_of_forall_exists_span

L177 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.fg_ideal_of_forall_exists_span

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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 fg_ideal_of_forall_exists_span {X : Scheme.{u}} (𝔞 : X.IdealSheafData)
    (hloc : ∀ x : X, ∃ V : X.affineOpens, x ∈ V.1 ∧
      ∃ g : Γ(X, V.1), 𝔞.ideal V = Ideal.span {g})
    (U : X.affineOpens) : (𝔞.ideal U).FG

theorem

ker_graphHom_fg

L230 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.ker_graphHom_fg

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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 ker_graphHom_fg (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) (U : (pullback c t).affineOpens) :
    ((graphHom a₀ h₀).ker.ideal U).FG

def

residualSheaf

L239 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.residualSheaf

Documentation

The residual ideal of D obtained by taking its colon by the graph ideal.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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

def residualSheaf {r : ℕ} (D : RelEffCartierDiv c (r + 1) t)
    (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) : (pullback c t).IdealSheafData

theorem

I_eq_ker_mul_residualSheaf

L243 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.I_eq_ker_mul_residualSheaf

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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 I_eq_ker_mul_residualSheaf {r : ℕ} (D : RelEffCartierDiv c (r + 1) t)
    (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
    (hle : D.I ≤ (graphHom a₀ h₀).ker) :
    D.I = (graphHom a₀ h₀).ker * residualSheaf D a₀ h₀

theorem

isClosedImmersion_inclusion

L261 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isClosedImmersion_inclusion

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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 isClosedImmersion_inclusion {X : Scheme.{u}} {I J : X.IdealSheafData} (h : I ≤ J) :
    IsClosedImmersion (Scheme.IdealSheafData.inclusion h)

theorem

le_residualSheaf

L267 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.le_residualSheaf

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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 le_residualSheaf {r : ℕ} (D : RelEffCartierDiv c (r + 1) t)
    (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) : D.I ≤ residualSheaf D a₀ h₀

theorem

isFinite_residualSheaf

L273 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isFinite_residualSheaf

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
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_residualSheaf {r : ℕ} (D : RelEffCartierDiv c (r + 1) t)
    (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) :
    IsFinite ((residualSheaf D a₀ h₀).subschemeι ≫ pullback.snd c t)

theorem

flat_ker_of_surjective

L289 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.flat_ker_of_surjective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
section moduleGrain
variable {R : Type*} [CommRing R]

Lean source · statement

theorem flat_ker_of_surjective {A B : Type*} [AddCommGroup A] [Module R A]
    [AddCommGroup B] [Module R B] [Module.Flat R A] [Module.Projective R B]
    (f : A →ₗ[R] B) (hf : Function.Surjective f) :
    Module.Flat R (LinearMap.ker f)

theorem

flat_localizedModule_of_flat

L306 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.flat_localizedModule_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_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
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

L326 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.hom_predicate_seam

Source context 8 commands

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

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

exists_affineOpen_le_span_nonZeroDivisor

L335 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.exists_affineOpen_le_span_nonZeroDivisor

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

theorem exists_affineOpen_le_span_nonZeroDivisor (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = 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),
        (graphHom a₀ h₀).ker.ideal W = Ideal.span {g}

theorem

graphHom_snd

L374 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.graphHom_snd

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem graphHom_snd (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) :
    graphHom a₀ h₀ ≫ pullback.snd c t = 𝟙 T

instance

isClosedImmersion_graphHom

L378 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isClosedImmersion_graphHom

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

instance isClosedImmersion_graphHom (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) :
    IsClosedImmersion (graphHom a₀ h₀)

instance

isIso_ker_graphHom_subschemeι_snd

L384 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isIso_ker_graphHom_subschemeι_snd

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

instance isIso_ker_graphHom_subschemeι_snd (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) :
    IsIso ((graphHom a₀ h₀).ker.subschemeι ≫ pullback.snd c t)

theorem

mk_subschemeObjIso_inclusion_appLE

L393 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.mk_subschemeObjIso_inclusion_appLE

Source context 8 commands

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

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

L419 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.presheaf_map_injective_of_eq

Source context 8 commands

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

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

L427 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.inclusion_app_mk_eq_zero_iff

Source context 8 commands

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

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

L448 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.subschemeObjIso_inv_mk_surjective

Source context 8 commands

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

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

finite_ker_of_surjective

L455 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.finite_ker_of_surjective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

theorem finite_ker_of_surjective {R : Type*} [CommRing R] {A B : Type*} [AddCommGroup A]
    [Module R A] [AddCommGroup B] [Module R B] [Module.Finite R A] [Module.Projective R B]
    (f : A →ₗ[R] B) (hf : Function.Surjective f) :
    Module.Finite R (LinearMap.ker f)

theorem

nonempty_linearEquiv_prod_of_surjective

L468 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.nonempty_linearEquiv_prod_of_surjective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

theorem nonempty_linearEquiv_prod_of_surjective {R : Type*} [CommRing R] {A B : Type*}
    [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [Module.Projective R B]
    (f : A →ₗ[R] B) (hf : Function.Surjective f) :
    Nonempty (A ≃ₗ[R] (LinearMap.ker f × B))

theorem

forall_finrank_eq_iff_of_isAffine

L489 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.forall_finrank_eq_iff_of_isAffine

Source context 8 commands

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

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

L506 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.forall_mem_finrank_eq_iff

Source context 8 commands

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

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

instance

algRA

L559 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.algRA

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance algRA : Algebra Rᵤ Aᵤ

instance

algAB

L563 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.algAB

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance algAB : Algebra Aᵤ Bᵤ

instance

algRB

L567 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.algRB

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance algRB : Algebra Rᵤ Bᵤ

instance

towerRAB

L572 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.towerRAB

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance towerRAB : IsScalarTower Rᵤ Aᵤ Bᵤ

instance

isFinite_subschemeι_comp_snd

L584 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isFinite_subschemeι_comp_snd

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

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

instance

flat_subschemeι_comp_snd

L587 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.flat_subschemeι_comp_snd

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance flat_subschemeι_comp_snd : Flat (D.I.subschemeι ≫ pullback.snd c t)

instance

algRC

L589 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.algRC

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance algRC : Algebra Rᵤ Cᵤ

theorem

flat_A

L594 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.flat_A

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem flat_A : Module.Flat Rᵤ Aᵤ

theorem

finite_A

L604 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.finite_A

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem finite_A : Module.Finite Rᵤ Aᵤ

theorem

inclusion_comp_eq_subschemeι

L613 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.inclusion_comp_eq_subschemeι

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

theorem inclusion_comp_eq_subschemeι :
    Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
      (D.I.subschemeι ≫ pullback.snd c t) =
    (residualSheaf D a₀ h₀).subschemeι ≫ pullback.snd c t

instance

isFinite_inclusion_comp

L619 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isFinite_inclusion_comp

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance isFinite_inclusion_comp :
    IsFinite (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
      (D.I.subschemeι ≫ pullback.snd c t))

theorem

finite_B

L625 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.finite_B

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

theorem finite_B : Module.Finite Rᵤ Bᵤ

theorem

inclusion_comp_eq_ker_subschemeι

L639 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.inclusion_comp_eq_ker_subschemeι

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem inclusion_comp_eq_ker_subschemeι :
    Scheme.IdealSheafData.inclusion hle ≫ (D.I.subschemeι ≫ pullback.snd c t) =
      (graphHom a₀ h₀).ker.subschemeι ≫ pullback.snd c t

instance

isIso_inclusion_comp

L644 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isIso_inclusion_comp

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance isIso_inclusion_comp :
    IsIso (Scheme.IdealSheafData.inclusion hle ≫ (D.I.subschemeι ≫ pullback.snd c t))

instance

isIso_app_inclusion_comp

L649 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.isIso_app_inclusion_comp

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance isIso_app_inclusion_comp :
    IsIso ((Scheme.IdealSheafData.inclusion hle ≫
      (D.I.subschemeι ≫ pullback.snd c t)).app U.1)

def

algEquivC

L655 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.algEquivC

Documentation

The sections of the graph subscheme are identified with the base sections via its projection.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

def algEquivC : Rᵤ ≃ₐ[Rᵤ] Cᵤ

instance

free_C

L664 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.free_C

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance free_C : Module.Free Rᵤ Cᵤ

instance

finite_C

L667 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.finite_C

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

instance finite_C : Module.Finite Rᵤ Cᵤ

theorem

inclusion_app_comp_algebraMap

L671 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.inclusion_app_comp_algebraMap

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ 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 hle).app
        ((D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)).hom.comp (algebraMap Rᵤ Aᵤ) =
      algebraMap Rᵤ Cᵤ

def

πC

L680 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.πC

Documentation

The restriction of sections from the divisor subscheme to the contained graph subscheme.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

def πC : Aᵤ →ₐ[Rᵤ] Cᵤ

theorem

πC_surjective

L692 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.πC_surjective

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem πC_surjective : Function.Surjective (πC D a₀ h₀ hle U)

def

kerπCEquiv

L699 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.kerπCEquiv

Documentation

The canonical linear equivalence between the ring kernel and linear kernel of this restriction.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

def kerπCEquiv : (RingHom.ker (πC D a₀ h₀ hle U).toRingHom) ≃ₗ[Rᵤ]
    ↥(LinearMap.ker (πC D a₀ h₀ hle U).toLinearMap)

theorem

flat_kerπC

L713 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.flat_kerπC

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem flat_kerπC : Module.Flat Rᵤ (RingHom.ker (πC D a₀ h₀ hle U).toRingHom)

theorem

finite_kerπC

L719 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.finite_kerπC

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem finite_kerπC : Module.Finite Rᵤ (RingHom.ker (πC D a₀ h₀ hle U).toRingHom)

instance

residualBasicOpenAlgebra

L727 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.residualBasicOpenAlgebra

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
section localizedChart

Lean source · statement

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

instance

divisorBasicOpenAlgebra

L740 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.divisorBasicOpenAlgebra

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
      Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    (((residualSheaf D a₀ h₀).subscheme.presheaf.map (homOfLE
      ((residualSheaf D a₀ h₀).subscheme.basicOpen_le _)).op).hom).toAlgebra

Lean source · statement

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

instance

residualBasicOpenAlgebraOverDivisor

L746 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.residualBasicOpenAlgebraOverDivisor

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
      Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    (((residualSheaf D a₀ h₀).subscheme.presheaf.map (homOfLE
      ((residualSheaf D a₀ h₀).subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ(D.I.subscheme,
  (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ(D.I.subscheme, D.I.subscheme.basicOpen h) :=
    ((D.I.subscheme.presheaf.map (homOfLE
      (D.I.subscheme.basicOpen_le h)).op).hom).toAlgebra

Lean source · statement

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

instance

divisorBasicOpenIsLocalization

L768 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.divisorBasicOpenIsLocalization

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
      Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    (((residualSheaf D a₀ h₀).subscheme.presheaf.map (homOfLE
      ((residualSheaf D a₀ h₀).subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ(D.I.subscheme,
  (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ(D.I.subscheme, D.I.subscheme.basicOpen h) :=
    ((D.I.subscheme.presheaf.map (homOfLE
      (D.I.subscheme.basicOpen_le h)).op).hom).toAlgebra
noncomputable local instance residualBasicOpenAlgebraOverDivisor (h : Aᵤ) : Algebra
  Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    ((algebraMap Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
        Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))).comp
      (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
        Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1))).toAlgebra

Lean source · statement

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

theorem

basicOpen_sections_equiv_kernel

L772 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.basicOpen_sections_equiv_kernel

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
      Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    (((residualSheaf D a₀ h₀).subscheme.presheaf.map (homOfLE
      ((residualSheaf D a₀ h₀).subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ(D.I.subscheme,
  (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ(D.I.subscheme, D.I.subscheme.basicOpen h) :=
    ((D.I.subscheme.presheaf.map (homOfLE
      (D.I.subscheme.basicOpen_le h)).op).hom).toAlgebra
noncomputable local instance residualBasicOpenAlgebraOverDivisor (h : Aᵤ) : Algebra
  Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    ((algebraMap Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
        Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))).comp
      (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
        Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1))).toAlgebra
local instance divisorBasicOpenIsLocalization (h : Aᵤ) :
    IsLocalization.Away h Γ(D.I.subscheme, D.I.subscheme.basicOpen h) :=
  (U.2.preimage (D.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)) (hgspan : (graphHom a₀ h₀).ker.ideal W = Ideal.span {g})
    (h : Aᵤ) (hhle : D.I.subscheme.basicOpen h ≤ D.I.subschemeι ⁻¹ᵁ W.1) :
    Nonempty (Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) ≃ₗ[Γ(D.I.subscheme,
                  (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)]
      ↥((RingHom.ker (πC D a₀ h₀ hle U).toRingHom).localized'
        Γ(D.I.subscheme, D.I.subscheme.basicOpen h) (Submonoid.powers h)
        (Algebra.linearMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
          Γ(D.I.subscheme, D.I.subscheme.basicOpen h))))

theorem

localizedModule_equiv_of_chart

L983 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.localizedModule_equiv_of_chart

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
section localizedChart
noncomputable local instance residualBasicOpenAlgebra (h : Aᵤ) : Algebra
      Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    (((residualSheaf D a₀ h₀).subscheme.presheaf.map (homOfLE
      ((residualSheaf D a₀ h₀).subscheme.basicOpen_le _)).op).hom).toAlgebra
noncomputable local instance divisorBasicOpenAlgebra (h : Aᵤ) : Algebra Γ(D.I.subscheme,
  (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ(D.I.subscheme, D.I.subscheme.basicOpen h) :=
    ((D.I.subscheme.presheaf.map (homOfLE
      (D.I.subscheme.basicOpen_le h)).op).hom).toAlgebra
noncomputable local instance residualBasicOpenAlgebraOverDivisor (h : Aᵤ) : Algebra
  Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
      Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h)) :=
    ((algebraMap Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1)
        Γ((residualSheaf D a₀ h₀).subscheme,
        (residualSheaf D a₀ h₀).subscheme.basicOpen
          (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
            Γ((residualSheaf D a₀ h₀).subscheme,
              (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
                (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1) h))).comp
      (algebraMap Γ(D.I.subscheme, (D.I.subschemeι ≫ pullback.snd c t) ⁻¹ᵁ U.1)
        Γ((residualSheaf D a₀ h₀).subscheme,
        (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
          (D.I.subschemeι ≫ pullback.snd c t)) ⁻¹ᵁ U.1))).toAlgebra
local instance divisorBasicOpenIsLocalization (h : Aᵤ) :
    IsLocalization.Away h Γ(D.I.subscheme, D.I.subscheme.basicOpen h) :=
  (U.2.preimage (D.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)) (hgspan : (graphHom a₀ h₀).ker.ideal W = Ideal.span {g})
    (h : Aᵤ) (hhle : D.I.subscheme.basicOpen h ≤ D.I.subschemeι ⁻¹ᵁ W.1) :
    Nonempty (LocalizedModule (Submonoid.powers h) Bᵤ ≃ₗ[Aᵤ]
      LocalizedModule (Submonoid.powers h) (RingHom.ker (πC D a₀ h₀ hle U).toRingHom))

theorem

exists_basicOpen_localizedModule_equiv

L1089 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.exists_basicOpen_localizedModule_equiv

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))

Lean source · statement

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

theorem

span_setOf_localizedModule_equiv_eq_top

L1109 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.span_setOf_localizedModule_equiv_eq_top

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ 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) Bᵤ ≃ₗ[Aᵤ]
      LocalizedModule (Submonoid.powers h) (RingHom.ker (πC D a₀ h₀ hle U).toRingHom))} =
    ⊤

theorem

flat_B

L1119 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.flat_B

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
include hle in

Lean source · statement

theorem flat_B : Module.Flat Rᵤ Bᵤ

theorem

rankAtStalk_A

L1130 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.rankAtStalk_A

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [IsSeparated c] [SmoothOfRelativeDimension 1 c] in

Lean source · statement

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

theorem

rankAtStalk_kerπC

L1135 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.rankAtStalk_kerπC

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
omit [SmoothOfRelativeDimension 1 c] in

Lean source · statement

theorem rankAtStalk_kerπC (x : PrimeSpectrum Rᵤ) :
    Module.rankAtStalk (R := Rᵤ) (RingHom.ker (πC D a₀ h₀ hle U).toRingHom) x = r

theorem

rankAtStalk_B

L1154 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.rankAtStalk_B

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
include hle in

Lean source · statement

theorem rankAtStalk_B (x : PrimeSpectrum Rᵤ) : Module.rankAtStalk (R := Rᵤ) Bᵤ x = r

theorem

finitePresentation_B

L1166 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.finitePresentation_B

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in
section chartModules
variable {r : ℕ} (D : RelEffCartierDiv c (r + 1) t) (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t)
  (hle : D.I ≤ (graphHom a₀ h₀).ker) (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))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫
        pullback.snd c t))))) (Subtype.val U)))
local notation "Bᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (residualSheaf D a₀ h₀))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion (le_residualSheaf D a₀ h₀) ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
local notation "Cᵤ" => Functor.obj (D := CommRingCat) (PresheafedSpace.presheaf
  (SheafedSpace.toPresheafedSpace
    (LocallyRingedSpace.toSheafedSpace (Scheme.toLocallyRingedSpace
      (Scheme.IdealSheafData.subscheme (Scheme.Hom.ker (graphHom a₀ h₀)))))))
  (Opposite.op (Functor.obj (TopologicalSpace.Opens.map (PresheafedSpace.Hom.base
    (LocallyRingedSpace.Hom.toHom
      (Scheme.Hom.toLRSHom (Scheme.IdealSheafData.inclusion hle ≫
        (Scheme.IdealSheafData.subschemeι (RelEffCartierDiv.I D) ≫ pullback.snd c t))))))
        (Subtype.val U)))
include hle in

Lean source · statement

theorem finitePresentation_B : Module.FinitePresentation Rᵤ Bᵤ

theorem

flat_residualSheaf

L1173 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.flat_residualSheaf

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

theorem flat_residualSheaf {r : ℕ} (D : RelEffCartierDiv c (r + 1) t)
    (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) (hle : D.I ≤ (graphHom a₀ h₀).ker) :
    Flat ((residualSheaf D a₀ h₀).subschemeι ≫ pullback.snd c t)

theorem

locallyOfFinitePresentation_residualSheaf

L1190 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.locallyOfFinitePresentation_residualSheaf

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

theorem locallyOfFinitePresentation_residualSheaf {r : ℕ} (D : RelEffCartierDiv c (r + 1) t)
    (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) (hle : D.I ≤ (graphHom a₀ h₀).ker) :
    LocallyOfFinitePresentation ((residualSheaf D a₀ h₀).subschemeι ≫ pullback.snd c t)

theorem

finrank_residualSheaf

L1213 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul.ResidualSplitting.finrank_residualSheaf

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_ker_graphOver_mul
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace ResidualSplitting
open _root_.AlgebraicGeometry.Scheme
variable {C S₀ : Scheme.{u}} {c : C ⟶ S₀}
  [IsSeparated c] [SmoothOfRelativeDimension 1 c]
  {T : Scheme.{u}} {t : T ⟶ S₀}
universe v in

Lean source · statement

theorem finrank_residualSheaf {r : ℕ} (D : RelEffCartierDiv c (r + 1) t)
    (a₀ : T ⟶ C) (h₀ : a₀ ≫ c = t) (hle : D.I ≤ (graphHom a₀ h₀).ker) (s : T) :
    ((residualSheaf D a₀ h₀).subschemeι ≫ pullback.snd c t).finrank s = r

theorem

exists_I_eq_ker_graphOver_mul

L1231 ↗

AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_ker_graphOver_mul

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_ker_graphOver_mul
    {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] [SmoothOfRelativeDimension 1 f] {r : ℕ}
    {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f (r + 1) g)
    (a : T ⟶ 𝒞) (ha : a ≫ f = g) (hle : D.I ≤ (graphOver f a ha).ker) :
    ∃ E : RelEffCartierDiv f r g, D.I = (graphOver f a ha).ker * E.I

Module documentation

Splitting a relative divisor along a section

Declarations