Commit 2025-10-21 20:48 df90d227

View on Github →

feat(RingTheory): meta properties of bijective ring homomorphisms (#28695) In particular, we show that bijective is a property local on the (algebraic) source.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

added theorem Algebra.algebraMapSubmonoid_self

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem AlgHom.coe_toLinearMap

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem TensorProduct.map_bijective

Modified Mathlib/RingTheory/LocalProperties/Exactness.lean

added theorem bijective_of_isLocalization_of_span_eq_top

added theorem injective_of_isLocalization_of_span_eq_top

added theorem surjective_of_isLocalization_of_span_eq_top

Modified Mathlib/RingTheory/Localization/Algebra.lean

added theorem IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ

added theorem IsLocalization.map_eq_toLinearMap_mapₐ

added theorem IsLocalization.map_linearMap_eq_toLinearMap_mapₐ

Modified Mathlib/RingTheory/Localization/Away/Basic.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Created Mathlib/RingTheory/RingHom/Bijective.lean

added theorem RingHom.Bijective.containsIdentities

added theorem RingHom.Bijective.isStableUnderBaseChange

added theorem RingHom.Bijective.ofLocalizationSpan

added theorem RingHom.Bijective.respectsIso

added theorem RingHom.Bijective.stableUnderComposition

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.includeLeft_bijective

added theorem Algebra.TensorProduct.includeRight_bijective

added theorem Algebra.TensorProduct.map_bijective