Structures · Algebra
Module.IsReflexive
A reflexive module is one for which the natural map to its double dual is a bijection.
Any finitely-generated projective module (and thus any finite-dimensional vector space)
is reflexive. See Module.instIsReflexiveOfFiniteOfProjective.
- Defined in
- Mathlib.LinearAlgebra.Dual.Defs
- Shape
- 2 explicit arguments · adds bijective_dual_eval'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by41
- Module.evalEquiv
- LinearEquiv.flip
- LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive
- Module.bijective_dual_eval
- Module.apply_evalEquiv_symm_apply
- LinearEquiv.flip_flip
- Module.mapEvalEquiv
- LinearEquiv.coe_toLinearMap_flip
- Module.evalEquiv_toLinearMap
- LinearEquiv.trans_dualMap_symm_flip
- Module.dualMap_dualMap_eq_iff_of_injective
- Module.mapEvalEquiv_symm_apply
- LinearMap.dualAnnihilator_ker_eq_range_flip
- Module.evalEquiv_apply
- Submodule.map_dualCoannihilator_linearEquiv_flip
- Module.IsReflexive.bijective_dual_eval'
- Module.dualMap_dualMap_eq_iff
- LinearEquiv.flip.congr_simp
- Module.symm_dualMap_evalEquiv
- Submodule.span_eq_top_of_ne_zero
- LinearMap.IsPerfPair.dualEval
- Submodule.map_dualAnnihilator_linearEquiv_flip_symm
- ULift.instModuleIsReflexive
- Prod.instModuleIsReflexive
- RootPairing.ofBilinear
- LinearEquiv.instIsPerfPair
- Module.IsReflexive.to_isTorsionFree
- Module.Dual.instIsReflecive
- LinearMap.IsPerfPair.id
- LinearEquiv.symm_flip
- Module.equiv
- Module.Dual.eval_comp_comp_evalEquiv_eq
- LinearMap.IsPerfPair.of_bijective
- Module.instFiniteDimensionalOfIsReflexive
- Module.evalEquiv.congr_simp
- Module.IsReflexive.of_split
- Module.erange_coe
- LinearEquiv.flip_apply
- Module.mapEvalEquiv_apply
- MulOpposite.instModuleIsReflexive
- Submodule.dualAnnihilator_map_linearEquiv_flip_symm
Ancestors0
No ancestors.