theorem
L31 ↗supportedIn_ofPoint
AlgebraicGeometry.RelEffCartierDiv.supportedIn_ofPoint
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_supportedIn_ofPoint
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.supportedIn_ofPoint
{𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} [IsSeparated f] {T : Scheme.{u}} {g : T ⟶ S}
(a : T ⟶ 𝒞) (ha : a ≫ f = g) (U : 𝒞.Opens) (hU : ∀ t : T, a t ∈ U) :
(RelEffCartierDiv.ofPoint f a ha).SupportedIn U