NYLL
Module

RelEffCartierDiv_comap_curveChange_ofPoint_eq_top_and_isIso_pullbackModuleComparison_of_disjoint.lean

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

Module documentation

Rel Eff Cartier Div comap curve Change of Point eq top and is Iso pullback Module

Comparison of disjoint

Imports7
Imported by1

Declarations

theorem

coe_support_ofPoint_I

L67 ↗
AlgebraicCurves.RelativeDivisors.Proofs.CartierDisjointBaseChange.AlgebraicGeometry.RelEffCartierDiv.coe_support_ofPoint_I
Source context 12 commands

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

section ProofImplementation
open _root_.AlgebraicCurves.RelativeDivisors.Proofs
namespace AlgebraicCurves.RelativeDivisors.Proofs.CartierDisjointBaseChange
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.isClosedImmersion_subschemeι_resProdMap
  AlgebraicGeometry.RelEffCartierDiv.isOpenImmersion_resProdMap
attribute [-simp] AlgebraicGeometry.RelEffCartierDiv.restrictAlong_extendAlong
  AlgebraicGeometry.RelEffCartierDiv.extendAlong_I
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_snd
  AlgebraicGeometry.RelEffCartierDiv.restrictAlong_I
  AlgebraicGeometry.RelEffCartierDiv.extendAlong_restrictAlong
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_fst_assoc
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_snd_assoc
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_fst
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry in
open scoped _root_.AlgebraicGeometry.RelEffCartierDiv in
Lean source · statement
theorem AlgebraicGeometry.RelEffCartierDiv.coe_support_ofPoint_I
    {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) [IsSeparated f] {T : Scheme.{u}} {g : T ⟶ S}
    (a : T ⟶ 𝒞) (ha : a ≫ f = g) :
    ((RelEffCartierDiv.ofPoint f a ha).I.support : Set ↥(pullback f g)) = Set.range (graphOver f a
      ha)
theorem

supportedIn_ofPoint_of_range_subset

L78 ↗
AlgebraicCurves.RelativeDivisors.Proofs.CartierDisjointBaseChange.AlgebraicGeometry.RelEffCartierDiv.supportedIn_ofPoint_of_range_subset
Source context 12 commands

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

section ProofImplementation
open _root_.AlgebraicCurves.RelativeDivisors.Proofs
namespace AlgebraicCurves.RelativeDivisors.Proofs.CartierDisjointBaseChange
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.isClosedImmersion_subschemeι_resProdMap
  AlgebraicGeometry.RelEffCartierDiv.isOpenImmersion_resProdMap
attribute [-simp] AlgebraicGeometry.RelEffCartierDiv.restrictAlong_extendAlong
  AlgebraicGeometry.RelEffCartierDiv.extendAlong_I
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_snd
  AlgebraicGeometry.RelEffCartierDiv.restrictAlong_I
  AlgebraicGeometry.RelEffCartierDiv.extendAlong_restrictAlong
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_fst_assoc
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_snd_assoc
  AlgebraicGeometry.RelEffCartierDiv.resProdMap_fst
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open scoped _root_.AlgebraicGeometry in
open scoped _root_.AlgebraicGeometry.RelEffCartierDiv in
Lean source · statement
theorem AlgebraicGeometry.RelEffCartierDiv.supportedIn_ofPoint_of_range_subset
    {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) [IsSeparated f] {T : Scheme.{u}} {g : T ⟶ S}
    (a : T ⟶ 𝒞) (ha : a ≫ f = g) (U : 𝒞.Opens) (haU : Set.range a ⊆ (U : Set 𝒞)) :
    (RelEffCartierDiv.ofPoint f a ha).SupportedIn U
theorem

comap_curveChange_ofPoint_eq_top_and_isIso_pullbackModuleComparison_of_disjoint

L104 ↗
AlgebraicGeometry.RelEffCartierDiv.comap_curveChange_ofPoint_eq_top_and_isIso_pullbackModuleComparison_of_disjoint
Source context 10 commands

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

section ProofImplementation
open _root_.AlgebraicCurves.RelativeDivisors.Proofs
open CartierDisjointBaseChange.AlgebraicGeometry.RelEffCartierDiv (
  supportedIn_ofPoint_of_range_subset)
namespace AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicCurves.RelativeDivisors.Proofs.CartierDisjointBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
Lean source · statement
theorem comap_curveChange_ofPoint_eq_top_and_isIso_pullbackModuleComparison_of_disjoint
    {R : Type u} [CommRing R] {C C'' : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of R)) (c'' : C'' ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (i'' : C'' ⟶ C) (hi'' : i'' ≫ c = c'') [IsClosedImmersion i'']
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (Q : T ⟶ C) (hQ : Q ≫ c = t)
    (hdisj : Disjoint (Set.range Q.base) (Set.range i''.base))
    (V : C.Opens) (hQV : Set.range Q.base ⊆ (V : Set C)) [SmoothOfRelativeDimension 1 (V.ι ≫ c)] :
    (RelEffCartierDiv.ofPoint c Q hQ).I.comap (RelPicard.curveChange i'' hi'' t) = ⊤ ∧
      IsIso ((RelEffCartierDiv.ofPoint c Q hQ).I.pullbackModuleComparison (RelPicard.curveChange
        i'' hi'' t))

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