Module

RelEffCartierDiv_exists_supportedIn_of_forall_finset.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_exists_supportedIn_of_forall_finset

2 declarations indexed from sourceView source ↗

Module documentation

Place relative divisors in an open that contains each finite set of interest.

Imports3

Mathlib.AlgebraicGeometry.Sites.Representability
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSupportedIn

Imported by2

theorem

exists_supportedIn_of_forall_finset_aux

L39 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_supportedIn_of_forall_finset.AlgebraicGeometry.RelEffCartierDiv.exists_supportedIn_of_forall_finset_aux

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_exists_supportedIn_of_forall_finset
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry

Lean source · statement

theorem exists_supportedIn_of_forall_finset_aux
    {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S)
    (hcov : ∀ (V : S.affineOpens) (F : Finset 𝒞), (∀ x ∈ F, f x ∈ (V : S.Opens)) →
      ∃ U : 𝒞.Opens, IsAffineOpen U ∧ U ≤ f ⁻¹ᵁ (V : S.Opens) ∧ ∀ x ∈ F, x ∈ U)
    (r : ℕ) {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) (t : T) :
    ∃ (W : T.Opens) (_ : t ∈ W) (V : S.affineOpens) (U : 𝒞.affineOpens)
      (_ : (U : 𝒞.Opens) ≤ f ⁻¹ᵁ (V : S.Opens)),
      (D.pullbackAlong W.ι rfl).SupportedIn U

theorem

exists_supportedIn_of_forall_finset

L72 ↗

AlgebraicGeometry.RelEffCartierDiv.exists_supportedIn_of_forall_finset

Source context 7 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.exists_supportedIn_of_forall_finset
    {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S)
    (hcov : ∀ (V : S.affineOpens) (F : Finset 𝒞), (∀ x ∈ F, f x ∈ (V : S.Opens)) →
      ∃ U : 𝒞.Opens, IsAffineOpen U ∧ U ≤ f ⁻¹ᵁ (V : S.Opens) ∧ ∀ x ∈ F, x ∈ U)
    (r : ℕ) {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g) (t : T) :
    ∃ (W : T.Opens) (_ : t ∈ W) (V : S.affineOpens) (U : 𝒞.affineOpens)
      (_ : (U : 𝒞.Opens) ≤ f ⁻¹ᵁ (V : S.Opens)),
      (D.pullbackAlong W.ι rfl).SupportedIn U

Module documentation

Declarations

exists_supportedIn_of_forall_finset_aux

exists_supportedIn_of_forall_finset