AlgebraicGeometry.Scheme.Hom.finrank_pullbackMap_of_comp_eq
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_Hom_finrank_pullbackMap_of_comp_eq
universe v w u
open CategoryTheory CategoryTheory.LimitsLean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Hom.finrank_pullbackMap_of_comp_eq {X X' S T :
AlgebraicGeometry.Scheme.{u}}
(f : X ⟶ S) (f' : X' ⟶ S) (t : T ⟶ S) (π : X' ⟶ X) (hπ : π ≫ f = f')
[AlgebraicGeometry.Flat π] [AlgebraicGeometry.IsFinite π] (y : ↑(pullback f t)) :
(pullback.map f' t f t π (𝟙 T) (𝟙 S) (by rw [Category.comp_id, hπ])
(by rw [Category.comp_id, Category.id_comp])).finrank y =
π.finrank (pullback.fst f t y) :=
AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback _ _ _ _
(CategoryTheory.IsPullback.fst_pullbackMap_of_comp_eq f f' t π hπ) y