Structures · Algebra
RootPairing.IsAnisotropic
We say a finite root pairing is anisotropic if there are no roots / coroots which have length
zero w.r.t. the root / coroot forms.
Examples include crystallographic pairings in characteristic zero
RootPairing.instIsAnisotropicOfIsCrystallographic and pairings over ordered scalars.
RootPairing.instIsAnisotropicOfLinearOrderedCommRing.
- Shape
- One type argument · adds rootForm_root_ne_zero, corootForm_coroot_ne_zero
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 by33
- RootPairing.toInvariantForm
- RootPairing.PolarizationEquiv
- RootPairing.disjoint_rootSpan_ker_rootForm
- RootPairing.finrank_corootSpan_eq'
- RootPairing.isCompl_rootSpan_ker_rootForm
- RootPairing.toInvariantForm_form
- RootPairing.IsAnisotropic.rootForm_root_ne_zero
- RootPairing.finrank_range_polarization_eq_finrank_span_coroot
- RootPairing.coroot_eq_polarizationEquiv_apply_root
- RootPairing.polarizationEquiv_apply
- RootPairing.rootForm_nondegenerate
- RootPairing.exists_coroot_ne
- RootPairing.polarizationEquiv_toLinearMap
- RootPairing.orthogonal_rootSpan_eq
- RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan
- RootPairing.Base.cartanMatrixIn_nondegenerate
- RootPairing.polarizationIn_Injective
- RootPairing.ker_rootForm_eq_dualAnnihilator
- RootPairing.rootSpan_eq_top_iff
- RootPairing.finrank_corootSpan_eq
- RootPairing.ker_corootForm_eq_dualAnnihilator
- RootPairing.linearIndepOn_coroot_iff
- RootPairing.disjoint_corootSpan_ker_corootForm
- RootPairing.PolarizationEquiv.congr_simp
- RootPairing.orthogonal_corootSpan_eq
- RootPairing.isCompl_corootSpan_ker_corootForm
- RootPairing.instIsBalanced
- RootPairing.smul_coroot_eq_of_root_add_root_eq
- RootPairing.toInvariantForm.congr_simp
- RootPairing.polarizationEquiv_symm_apply_coroot
- RootPairing.IsAnisotropic.corootForm_coroot_ne_zero
- RootPairing.rootForm_restrict_nondegenerate_of_isAnisotropic
- RootPairing.instIsAnisotropicFlip
Ancestors0
No ancestors.