Structures · Algebra
Algebra.IsInvariant
An action of a group G on an extension of rings B/A is invariant if every fixed point of
B lies in the image of A. The converse statement that every point in the image of A is fixed
by G is smul_algebraMap (assuming SMulCommClass A B G).
- Defined in
- Mathlib.RingTheory.Invariant.Defs
- Shape
- 3 explicit arguments · adds isInvariant
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
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 by30
- Algebra.IsInvariant.isInvariant
- Algebra.IsInvariant.isIntegral
- Algebra.IsInvariant.exists_smul_of_under_eq
- arithFrobAt
- Algebra.IsInvariant.charpoly_mem_lifts
- Ideal.IsFractionRing.normal
- IsArithFrobAt.exists_primesOver_isConj
- IsFractionRing.stabilizerQuotientInertiaEquiv
- Ideal.IsFractionRing.finite_of_isInvariant
- IsFractionRing.isInvariant_of_isIntegral
- IsFractionRing.stabilizerHom_surjective
- Algebra.IsInvariant.orbit_eq_primesOver
- Ideal.Quotient.stabilizerQuotientInertiaEquiv
- IsArithFrobAt.exists_of_isInvariant
- Ideal.Quotient.stabilizerHom_surjective
- Ideal.Quotient.exists_algHom_fixedPoint_quotient_under
- IsArithFrobAt.arithFrobAt
- instIsInvariantSubtypeMemSubalgebraSubalgebraSubgroupQuotient
- IsFractionRing.isInvariant
- IsArithFrobAt.arithFrobAt_mem_stabilizer
- Ideal.Quotient.normal
- IsFractionRing.stabilizerQuotientInertiaEquiv_mk
- Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite
- isConj_arithFrobAt
- Ideal.Quotient.finite_of_isInvariant
- Ideal.Quotient.stabilizerHom_surjective_of_profinite
- Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk
- instNonemptyObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor
- Algebra.IsInvariant.isIntegral_of_profinite
- Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under
Ancestors0
No ancestors.