Module

RelEffCartierDiv_exists_I_eq_prodKerGraph_and_supportedIn.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_I_eq_prodKerGraph_and_supportedIn

2 declarations indexed from sourceView source ↗

Module documentation

Rel Eff Cartier Div exists I eq prod Ker Graph and supported In

Imports6

Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSum
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSupportedIn
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_supportedIn_I_eq_mul_of_supportedIn

Imported by2

theorem

supportedIn_ofPoint

L64 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_I_eq_prodKerGraph_and_supportedIn.FltWs21.M10b.supportedIn_ofPoint

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_exists_I_eq_prodKerGraph_and_supportedIn
attribute [-instance]
  instNeg
  instSMulInt
  instAddCommGroup
  instAdd
  instSub
  instModuleCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  instSMulCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTop
  instSMulNat
  instZero
attribute [-simp] AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.sub_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sresTop
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.add_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.IdealSheafData.coe_resLE
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.smul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_ofLE_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.ideal_range
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zero_app
  AlgebraicGeometry.Scheme.IdealSheafData.sres_sres
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.comp_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.neg_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.id_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.coe_mulRight_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.nsmul_app
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.mk.injEq
  AlgebraicGeometry.Scheme.IdealSheafData.IdealHom.zsmul_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace FltWs21
namespace M10b

Lean source · statement

theorem supportedIn_ofPoint {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] (U : 𝒞.Opens)
    {T : Scheme.{u}} {g : T ⟶ S} (a : T ⟶ 𝒞) (ha : a ≫ f = g) (haU : Set.range a.base ⊆ (U : Set
      𝒞)) :
    (RelEffCartierDiv.ofPoint f a ha).SupportedIn U

theorem

exists_I_eq_prodKerGraph_and_supportedIn

L80 ↗

AlgebraicGeometry.RelEffCartierDiv.exists_I_eq_prodKerGraph_and_supportedIn

Source context 7 commands