theorem
L32 ↗pullbackAlong_injective
AlgebraicGeometry.RelEffCartierDiv.pullbackAlong_injective
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_pullbackAlong_injective
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry inLean source · full declaration
theorem _root_.AlgebraicGeometry.RelEffCartierDiv.pullbackAlong_injective
{𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S} {r : ℕ} {T T' : Scheme.{u}} {g : T ⟶ S} {g' : T' ⟶ S}
(φ : T ⟶ T') (hφ : φ ≫ g' = g) [Flat φ] [Surjective φ] :
Function.Injective fun D : RelEffCartierDiv f r g' => D.pullbackAlong φ hφ := by
intro D E h
have hI := congrArg RelEffCartierDiv.I h
change D.I.comap (mapOnProdOver f φ hφ) = E.I.comap (mapOnProdOver f φ hφ) at hI
have : Flat (mapOnProdOver f φ hφ) :=
MorphismProperty.of_isPullback (isPullback_mapOnProdOver f φ hφ).flip inferInstance
have : Surjective (mapOnProdOver f φ hφ) :=
MorphismProperty.of_isPullback (isPullback_mapOnProdOver f φ hφ).flip inferInstance
exact RelEffCartierDiv.ext
(Scheme.IdealSheafData.comap_injective_of_flat_of_surjective (mapOnProdOver f φ hφ) hI)