Commit 2024-10-29 10:42 925146c7

View on Github →

chore(GroupTheory/GroupAction): split off Defs file (#18345) The goal of this PR is to have a file with the definitions for the orbit and stabilizer of a group, and enough theory to define quotient groups.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/CategoryTheory/Galois/GaloisObjects.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean

Modified Mathlib/Dynamics/Minimal.lean

Modified Mathlib/GroupTheory/Coset/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

deleted def FixedPoints.addSubgroup

deleted theorem FixedPoints.addSubgroup_toAddSubmonoid

deleted def FixedPoints.addSubmonoid

deleted theorem FixedPoints.mem_addSubgroup

deleted theorem FixedPoints.mem_addSubmonoid

deleted theorem FixedPoints.mem_subgroup

deleted theorem FixedPoints.mem_submonoid

deleted def FixedPoints.subgroup

deleted theorem FixedPoints.subgroup_toSubmonoid

deleted def FixedPoints.submonoid

deleted theorem MulAction.disjoint_image_image_iff

deleted def MulAction.fixedBy

deleted def MulAction.fixedPoints

deleted theorem MulAction.fixed_eq_iInter_fixedBy

deleted theorem MulAction.image_inter_image_iff

deleted theorem MulAction.le_stabilizer_smul_left

deleted theorem MulAction.le_stabilizer_smul_right

deleted theorem MulAction.mapsTo_smul_orbit

deleted theorem MulAction.mem_fixedBy

deleted theorem MulAction.mem_fixedPoints'

deleted theorem MulAction.mem_fixedPoints

deleted theorem MulAction.mem_orbit

deleted theorem MulAction.mem_orbit_iff

deleted theorem MulAction.mem_orbit_of_mem_orbit_subgroup

deleted theorem MulAction.mem_orbit_of_mem_orbit_submonoid

deleted theorem MulAction.mem_orbit_self

deleted theorem MulAction.mem_orbit_smul

deleted theorem MulAction.mem_orbit_symm

deleted theorem MulAction.mem_stabilizerSubmonoid_iff

deleted theorem MulAction.mem_stabilizer_iff

deleted theorem MulAction.mem_subgroup_orbit_iff

deleted theorem MulAction.orbit.coe_smul

deleted def MulAction.orbit

deleted theorem MulAction.orbitRel.Quotient.mem_orbit

deleted theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff'

deleted theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff

deleted theorem MulAction.orbitRel.Quotient.orbit.coe_smul

deleted theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out

deleted theorem MulAction.orbitRel.Quotient.orbit_inj

deleted theorem MulAction.orbitRel.Quotient.orbit_injective

deleted theorem MulAction.orbitRel.Quotient.orbit_mk

deleted theorem MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff

deleted theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq'

deleted theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq

deleted def MulAction.orbitRel

deleted theorem MulAction.orbitRel_apply

deleted theorem MulAction.orbit_eq_iff

deleted theorem MulAction.orbit_nonempty

deleted theorem MulAction.orbit_smul

deleted theorem MulAction.orbit_smul_subset

deleted theorem MulAction.orbit_subgroup_subset

deleted theorem MulAction.orbit_submonoid_subset

deleted theorem MulAction.quotient_preimage_image_eq_union_mul

deleted def MulAction.selfEquivSigmaOrbits'

deleted def MulAction.selfEquivSigmaOrbits

deleted theorem MulAction.smul_mem_orbit_smul

deleted theorem MulAction.smul_orbit_subset

deleted def MulAction.stabilizer

deleted def MulAction.stabilizerSubmonoid

deleted theorem MulAction.stabilizer_mul_eq_left

deleted theorem MulAction.stabilizer_mul_eq_right

deleted theorem MulAction.stabilizer_smul_eq_left

deleted theorem MulAction.stabilizer_smul_eq_right

deleted theorem MulAction.univ_eq_iUnion_orbit

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

Created Mathlib/GroupTheory/GroupAction/Defs.lean

added def FixedPoints.addSubgroup

added theorem FixedPoints.addSubgroup_toAddSubmonoid

added def FixedPoints.addSubmonoid

added theorem FixedPoints.mem_addSubgroup

added theorem FixedPoints.mem_addSubmonoid

added theorem FixedPoints.mem_subgroup

added theorem FixedPoints.mem_submonoid

added def FixedPoints.subgroup

added theorem FixedPoints.subgroup_toSubmonoid

added def FixedPoints.submonoid

added theorem MulAction.disjoint_image_image_iff

added def MulAction.fixedBy

added def MulAction.fixedPoints

added theorem MulAction.fixed_eq_iInter_fixedBy

added theorem MulAction.image_inter_image_iff

added theorem MulAction.le_stabilizer_smul_left

added theorem MulAction.le_stabilizer_smul_right

added theorem MulAction.mapsTo_smul_orbit

added theorem MulAction.mem_fixedBy

added theorem MulAction.mem_fixedPoints'

added theorem MulAction.mem_fixedPoints

added theorem MulAction.mem_orbit

added theorem MulAction.mem_orbit_iff

added theorem MulAction.mem_orbit_of_mem_orbit_subgroup

added theorem MulAction.mem_orbit_of_mem_orbit_submonoid

added theorem MulAction.mem_orbit_self

added theorem MulAction.mem_orbit_smul

added theorem MulAction.mem_orbit_symm

added theorem MulAction.mem_stabilizerSubmonoid_iff

added theorem MulAction.mem_stabilizer_iff

added theorem MulAction.mem_subgroup_orbit_iff

added theorem MulAction.orbit.coe_smul

added def MulAction.orbit

added theorem MulAction.orbitRel.Quotient.mem_orbit

added theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff'

added theorem MulAction.orbitRel.Quotient.mem_subgroup_orbit_iff

added theorem MulAction.orbitRel.Quotient.orbit.coe_smul

added theorem MulAction.orbitRel.Quotient.orbit_eq_orbit_out

added theorem MulAction.orbitRel.Quotient.orbit_inj

added theorem MulAction.orbitRel.Quotient.orbit_injective

added theorem MulAction.orbitRel.Quotient.orbit_mk

added theorem MulAction.orbitRel.Quotient.subgroup_quotient_eq_iff

added theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq'

added theorem MulAction.orbitRel.quotient_eq_of_quotient_subgroup_eq

added def MulAction.orbitRel

added theorem MulAction.orbitRel_apply

added theorem MulAction.orbit_eq_iff

added theorem MulAction.orbit_nonempty

added theorem MulAction.orbit_smul

added theorem MulAction.orbit_smul_subset

added theorem MulAction.orbit_subgroup_subset

added theorem MulAction.orbit_submonoid_subset

added theorem MulAction.quotient_preimage_image_eq_union_mul

added def MulAction.selfEquivSigmaOrbits'

added def MulAction.selfEquivSigmaOrbits

added theorem MulAction.smul_mem_orbit_smul

added theorem MulAction.smul_orbit_subset

added def MulAction.stabilizer

added def MulAction.stabilizerSubmonoid

added theorem MulAction.stabilizer_mul_eq_left

added theorem MulAction.stabilizer_mul_eq_right

added theorem MulAction.stabilizer_smul_eq_left

added theorem MulAction.stabilizer_smul_eq_right

added theorem MulAction.univ_eq_iUnion_orbit

Modified Mathlib/GroupTheory/GroupAction/FixedPoints.lean

Modified Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

Modified Mathlib/GroupTheory/Perm/ClosureSwap.lean

Modified Mathlib/GroupTheory/Perm/DomMulAct.lean

Modified Mathlib/Topology/Algebra/ConstMulAction.lean