Commit 2024-10-14 12:17 134f2f10

View on Github →

feat: add RingTheory.Trace.Quotient: relations between trace maps and quotients (#14798) We add a file RingTheory.Trace.Quotient gathering results about the relations between the trace map on B → A and the trace map on quotients and localizations.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem finrank_le_of_span_eq_top

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

modified theorem AddMonoidHom.map_trace

Modified Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean

added theorem isIntegrallyClosed_of_isLocalization

Created Mathlib/RingTheory/LocalRing/Quotient.lean

added def LocalRing.basisQuotient

added theorem LocalRing.basisQuotient_apply

added theorem LocalRing.basisQuotient_repr

added theorem LocalRing.finrank_quotient_map

added theorem LocalRing.quotient_span_eq_top_iff_span_eq_top

Created Mathlib/RingTheory/Trace/Quotient.lean

added theorem Algebra.trace_quotient_eq_of_isDedekindDomain

added theorem Algebra.trace_quotient_mk

added theorem IsLocalization.AtPrime.map_eq_maximalIdeal

added theorem comap_map_eq_map_of_isLocalization_algebraMapSubmonoid

added def equivQuotMaximalIdealOfIsLocalization

added def quotMapEquivQuotMapMaximalIdealOfIsLocalization

added theorem trace_quotient_eq_trace_localization_quotient