Commit 2024-11-04 13:07 100b9268

View on Github →

feat(AlgebraicGeometry): pre-requisites of description of topological space of pullback (#18255)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Created Mathlib/Algebra/Category/Ring/LinearAlgebra.lean

added theorem CommRingCat.nontrivial_of_isPushout_of_isField

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

added theorem AlgebraicGeometry.isPullback_Spec_map_isPushout

added theorem AlgebraicGeometry.isPullback_Spec_map_pushout

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat.lean

modified theorem Module.FaithfullyFlat.of_linearEquiv