Structures · Algebra
IsLocalizedModule
The characteristic predicate for localized module.
IsLocalizedModule S f describes that f : M ⟶ M' is the localization map identifying M' as
LocalizedModule S M.
- Shape
- 2 explicit arguments · adds map_units, surj, exists_of_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Int
- CommRingCat.carrier
How is a type an instance?
Loading the hierarchy index…
Assumed by232
- IsLocalizedModule.map
- IsLocalizedModule.mk'
- IsLocalizedModule.map_units
- Submodule.localized'
- Submodule.localized₀
- IsLocalizedModule.iso
- IsLocalizedModule.surj
- IsLocalizedModule.map_apply
- IsLocalizedModule.mk'_surjective
- IsLocalizedModule.mk'_one
- IsLocalizedModule.linearEquiv
- IsLocalizedModule.fromLocalizedModule
- IsLocalizedModule.lift
- IsLocalizedModule.exists_of_eq
- IsLocalizedModule.isBaseChange
- IsLocalizedModule.mapExtendScalars
- IsLocalizedModule.map_mk'
- IsLocalizedModule.eq_iff_exists
- IsLocalizedModule.linearMap_ext
- IsLocalizedModule.lift_rank_eq
- Submodule.toLocalized'
- IsLocalizedModule.mk'_cancel'
- IsLocalizedModule.mk'_smul
- IsLocalizedModule.liftOfLE
- IsLocalizedModule.iso_mk_one
- IsLocalizedModule.map_comp
- IsLocalizedModule.smul_inj
- IsLocalizedModule.mapExtendScalars_apply_apply
- IsLocalizedModule.lift_apply
- LinearMap.range_localizedMap_eq_localized₀_range
- IsLocalizedModule.iso_symm_comp
- IsLocalizedModule.fromLocalizedModule'
- IsLocalizedModule.mk'_cancel_left
- Module.eq_of_localization_maximal
- Module.subsingleton_of_localization_maximal
- IsLocalizedModule.mk'_eq_iff
- LocalizedModule.coe_map_eq
- Module.Basis.ofIsLocalizedModule_apply
- IsLocalizedModule.mk'_zero
- IsLocalizedModule.lift_comp
- Module.Basis.ofIsLocalizedModule
- Submodule.mem_of_localization_maximal
- Submodule.eq_of_localization₀_maximal
- Submodule.localized'_top
- LinearMap.localized'_ker_eq_ker_localizedMap
- Module.FinitePresentation.exists_lift_of_isLocalizedModule
- exists_bijective_map_powers
- IsLocalizedModule.mk'_smul_mk'
- Submodule.toLocalized'_apply_coe
- Submodule.localized₀_bot
Ancestors0
No ancestors.