Commit 2023-12-04 12:41 3ce1e1f9

View on Github →

feat(Algebra/DirectLimit): add map, congr, lift_injective for direct limits of modules, abelian groups and rings (#8692) Consider direct limits lim G and lim G' with direct system f and f' respectively, any family of linear maps gᵢ : Gᵢ ⟶ G'ᵢ such that g ∘ f = f' ∘ g induces a linear map lim G ⟶ lim G'. When gᵢ's are equivalence, so is the induced. Similarly for direct limits of groups and rings This PR is splitted from #8473

Estimated changes

Modified Mathlib/Algebra/DirectLimit.lean

added def AddCommGroup.DirectLimit.congr

added theorem AddCommGroup.DirectLimit.congr_apply_of

added theorem AddCommGroup.DirectLimit.congr_symm_apply_of

modified def AddCommGroup.DirectLimit.lift

added theorem AddCommGroup.DirectLimit.lift_injective

added def AddCommGroup.DirectLimit.map

added theorem AddCommGroup.DirectLimit.map_apply_of

added theorem AddCommGroup.DirectLimit.map_comp

added theorem AddCommGroup.DirectLimit.map_id

modified def AddCommGroup.DirectLimit.of

added def Module.DirectLimit.congr

added theorem Module.DirectLimit.congr_apply_of

added theorem Module.DirectLimit.congr_symm_apply_of

added theorem Module.DirectLimit.lift_injective

added def Module.DirectLimit.map

added theorem Module.DirectLimit.map_apply_of

added theorem Module.DirectLimit.map_comp

added theorem Module.DirectLimit.map_id

added def Ring.DirectLimit.congr

added theorem Ring.DirectLimit.congr_apply_of

added theorem Ring.DirectLimit.congr_symm_apply_of

added theorem Ring.DirectLimit.lift_injective

added def Ring.DirectLimit.map

added theorem Ring.DirectLimit.map_apply_of

added theorem Ring.DirectLimit.map_comp

added theorem Ring.DirectLimit.map_id