Scheme_Hom_finrank_morphismRestrict_eq_finrank.lean

theorem finrank_tensorProduct_eq_of_algEquiv {A : Type*} [CommRing A] {R R' : Type*}
  [CommRing R] [CommRing R']
    [Algebra A R] [Algebra A R'] (e : R ≃ₐ[A] R') (M : Type*) [AddCommGroup M] [Module A M] :
    Module.finrank R (R ⊗[A] M) = Module.finrank R' (R' ⊗[A] M)

theorem rankAtStalk_eq_of_isLocalizedModule {A A' : Type*} [CommRing A] [CommRing A']
  [Algebra A A']
    (S : Submonoid A) [IsLocalization S A'] {M M' : Type*} [AddCommGroup M] [Module A M]
      [AddCommGroup M']
    [Module A M'] [Module A' M'] [IsScalarTower A A' M'] (f : M →ₗ[A] M') [IsLocalizedModule S f]
    (p : PrimeSpectrum A') :
    Module.rankAtStalk (R := A') M' p = Module.rankAtStalk (R := A) M (p.comap (algebraMap A A'))

theorem finrank_eq_of_isPushout_of_away {R B T P : CommRingCat.{u}} {φ : R ⟶ B} {ψ : R ⟶ T}
    {inl : B ⟶ P} {inr : T ⟶ P} (h : IsPushout φ ψ inl inr) (r : R)
    (hT : letI := ψ.hom.toAlgebra; IsLocalization.Away r T) (x : PrimeSpectrum T) :
    inr.hom.finrank x = φ.hom.finrank (PrimeSpectrum.comap ψ.hom x) := by
  algebraize [φ.hom, ψ.hom, inl.hom, inr.hom, inl.hom.comp φ.hom]
  have : IsScalarTower R T P := .of_algebraMap_eq' <| congr($(h.1.1).hom)
  have : Algebra.IsPushout R B T P := CommRingCat.isPushout_iff_isPushout.mp h
  have : Algebra.IsPushout R T B P := Algebra.IsPushout.symm inferInstance
  have hbc : IsBaseChange T (IsScalarTower.toAlgHom R B P).toLinearMap := Algebra.IsPushout.out
  have : IsLocalization.Away r T := hT
  have : IsLocalizedModule (Submonoid.powers r) (IsScalarTower.toAlgHom R B P).toLinearMap :=
    (isLocalizedModule_iff_isBaseChange (Submonoid.powers r) T _).mpr hbc
  change Module.rankAtStalk (R := T) P x = Module.rankAtStalk (R := R) B _
  exact rankAtStalk_eq_of_isLocalizedModule (Submonoid.powers r) (IsScalarTower.toAlgHom R B
    P).toLinearMap x

theorem _root_.AlgebraicGeometry.Scheme.Hom.finrank_morphismRestrict_eq_finrank
    {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f] (W : S.Opens) [Flat (f ∣_ W)] (s : S) (hs : s ∈ W) :
    (f ∣_ W).finrank ⟨s, hs⟩ = f.finrank s