theorem
L29 ↗pullback_of_comp_eq
AlgebraicGeometry.Polarisation.LocIsoOnBase.pullback_of_comp_eq
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.Polarisation_LocIsoOnBase_pullback_of_comp_eq
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.Polarisation
universe uLean source · statement
theorem _root_.AlgebraicGeometry.Polarisation.LocIsoOnBase.pullback_of_comp_eq
{S S' : Type u} [CommRing S] [CommRing S'] {X Y : Scheme.{u}}
{g : X ⟶ Spec (CommRingCat.of S)} (g' : Y ⟶ Spec (CommRingCat.of S')) (h : Y ⟶ X)
(φ : Spec (CommRingCat.of S') ⟶ Spec (CommRingCat.of S)) (comm : h ≫ g = g' ≫ φ)
{M M' : X.Modules} (hM : LocIsoOnBase g M M') :
LocIsoOnBase g' ((Scheme.Modules.pullback h).obj M) ((Scheme.Modules.pullback h).obj M')