Commit 2026-05-10 12:46 1b6244ba

View on Github →

feat(AlgebraicGeometry): rank of finite flat morphism (#38090) From Pi1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Tower.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added theorem AlgebraicGeometry.Scheme.exists_Spec_apply_eq

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

added theorem AlgebraicGeometry.IsAffine.of_isPullback

added theorem AlgebraicGeometry.isPushout_appTop_of_isPullback

Modified Mathlib/AlgebraicGeometry/Morphisms/Finite.lean

added theorem AlgebraicGeometry.Scheme.Hom.finite_appTop

Modified Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean

added theorem AlgebraicGeometry.LocallyOfFinitePresentation.SpecMap_iff

added theorem AlgebraicGeometry.Scheme.Hom.finitePresentation_appTop

Modified Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

added theorem AlgebraicGeometry.Flat.SpecMap_iff

added theorem AlgebraicGeometry.Scheme.Hom.flat_appTop

Created Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean

added def AlgebraicGeometry.Scheme.Hom.finrank

added theorem AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_algebraMap

added theorem AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank

added theorem AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso

added theorem AlgebraicGeometry.Scheme.Hom.finrank_eq_one_of_isIso

added theorem AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback

added theorem AlgebraicGeometry.Scheme.Hom.finrank_pullback_fst

added theorem AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

added theorem CategoryTheory.IsPullback.map_fst_comp_fst_snd_comp_fst

added theorem CategoryTheory.IsPullback.paste_twist_right

Modified Mathlib/RingTheory/Flat/Rank.lean

added theorem Algebra.rankAtStalk_eq_of_isPushout

added theorem CommRingCat.finrank_eq_of_isPushout

added theorem RingHom.finrank_algebraMap

added theorem RingHom.finrank_comp_left_of_bijective

added theorem RingHom.finrank_comp_right_of_bijective

Modified Mathlib/RingTheory/Localization/BaseChange.lean

added theorem Algebra.IsPushout.of_bijective_left

added theorem Algebra.IsPushout.of_bijective_right

added theorem Algebra.algebraMapSubmonoid_isUnit_le_isUnit

added theorem Submonoid.map_isUnit_le_isUnit