Commit 2024-06-11 14:59 965c7f81

View on Github →

feat(RingTheory/AdicCompletion): functoriality (#12543) Adds functoriality of adic completions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

added theorem DirectSum.of_apply

added theorem DirectSum.sum_univ_of

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

added theorem AdicCompletion.val_smul_eq_evalₐ_smul

Created Mathlib/RingTheory/AdicCompletion/Functoriality.lean

added def AdicCompletion.AdicCauchySequence.map

added theorem AdicCompletion.AdicCauchySequence.map_comp

added theorem AdicCompletion.AdicCauchySequence.map_comp_apply

added theorem AdicCompletion.AdicCauchySequence.map_id

added theorem AdicCompletion.component_sumInv

added def AdicCompletion.congr

added theorem AdicCompletion.congr_apply

added theorem AdicCompletion.congr_symm_apply

added def AdicCompletion.map

added theorem AdicCompletion.map_comp

added theorem AdicCompletion.map_comp_apply

added theorem AdicCompletion.map_ext''

added theorem AdicCompletion.map_ext'

added theorem AdicCompletion.map_ext

added theorem AdicCompletion.map_id

added theorem AdicCompletion.map_mk

added theorem AdicCompletion.map_val_apply

added def AdicCompletion.pi

added def AdicCompletion.piEquivFin

added theorem AdicCompletion.piEquivFin_apply

added def AdicCompletion.piEquivOfFintype

added theorem AdicCompletion.piEquivOfFintype_apply

added def AdicCompletion.sum

added def AdicCompletion.sumEquivOfFintype

added theorem AdicCompletion.sumEquivOfFintype_apply

added theorem AdicCompletion.sumEquivOfFintype_symm_apply

added def AdicCompletion.sumInv

added theorem AdicCompletion.sumInv_apply

added theorem AdicCompletion.sumInv_comp_sum

added theorem AdicCompletion.sum_comp_sumInv

added theorem AdicCompletion.sum_lof

added theorem AdicCompletion.sum_of

added theorem AdicCompletion.transitionMap_comp_reduceModIdeal

added theorem AdicCompletion.val_sum

added def LinearMap.reduceModIdeal

added theorem LinearMap.reduceModIdeal_apply