Module

RelEffCartierDiv_isOpenImmersion_presheaf_supportedIn_incl.lean

Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_isOpenImmersion_presheaf_supportedIn_incl

2 declarations indexed from sourceView source ↗

Module documentation

The inclusion of divisors supported in an open is an open immersion of presheaves.

Imports3

Mathlib.AlgebraicGeometry.Sites.Representability
Mathlib.CategoryTheory.Limits.Types.Pullbacks
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivSupportedIn

Imported by2

theorem

isOpenImmersion_presheaf_supportedIn_incl_aux

L43 ↗

AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_isOpenImmersion_presheaf_supportedIn_incl.AlgebraicGeometry.RelEffCartierDiv.isOpenImmersion_presheaf_supportedIn_incl_aux

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs
namespace RelEffCartierDiv_isOpenImmersion_presheaf_supportedIn_incl
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
variable {𝒞 S : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (U : 𝒞.Opens)

Lean source · statement

theorem isOpenImmersion_presheaf_supportedIn_incl_aux :
    IsOpenImmersion.presheaf (RelEffCartierDiv.supportedIn f r U).ι

theorem

isOpenImmersion_presheaf_supportedIn_incl

L91 ↗

AlgebraicGeometry.RelEffCartierDiv.isOpenImmersion_presheaf_supportedIn_incl

Source context 8 commands

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

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

Lean source · statement

theorem _root_.AlgebraicGeometry.RelEffCartierDiv.isOpenImmersion_presheaf_supportedIn_incl {𝒞 S
    : Scheme.{u}} (f : 𝒞 ⟶ S) (r : ℕ) (U : 𝒞.Opens) :
    IsOpenImmersion.presheaf (RelEffCartierDiv.supportedIn f r U).ι

Module documentation

Declarations

isOpenImmersion_presheaf_supportedIn_incl_aux

isOpenImmersion_presheaf_supportedIn_incl