This file isolates the group-theoretic index calculation used in abstract valuation theory. For a homomorphism d, an inclusion L ≤ K splits its relative index into the index of the images under d and the relative index inside ker d.
The natural-valued Subgroup.relIndex is useful only after finiteness is known: it represents every infinite index by zero. The following API keeps the actual coset cardinality and is therefore the source for general tower and image--kernel laws. Chosen representatives occur only in private equivalences used to prove these canonical equalities.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def kernelToSaturation (d : G →* D) (L K : Subgroup G) :
↑(K ⊓ d.ker) →* ↑(K ⊓ (L ⊔ d.ker))Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem kernelToSaturation_rel_iff (d : G →* D) (L K : Subgroup G)
(x y : ↑(K ⊓ d.ker)) :
QuotientGroup.leftRel ((L ⊓ d.ker).subgroupOf (K ⊓ d.ker)) x y ↔
QuotientGroup.leftRel (L.subgroupOf (K ⊓ (L ⊔ d.ker)))
(kernelToSaturation d L K x) (kernelToSaturation d L K y)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def kernelCosetToSaturationCoset (d : G →* D) (L K : Subgroup G) :
(↑(K ⊓ d.ker) ⧸ (L ⊓ d.ker).subgroupOf (K ⊓ d.ker)) →
(↑(K ⊓ (L ⊔ d.ker)) ⧸ L.subgroupOf (K ⊓ (L ⊔ d.ker)))Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem kernelCosetToSaturationCoset_injective (d : G →* D) (L K : Subgroup G) :
Function.Injective (kernelCosetToSaturationCoset d L K)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem kernelCosetToSaturationCoset_surjective (d : G →* D) {L K : Subgroup G}
(hLK : L ≤ K) : Function.Surjective (kernelCosetToSaturationCoset d L K)The kernel cosets for L ≤ K are the cosets in the part of K saturated by ker d.
This is the set-level second-isomorphism argument needed for relative indices; no normality assumption on L is required.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def kernelCosetEquivSaturation (d : G →* D) {L K : Subgroup G} (hLK : L ≤ K) :
(↑(K ⊓ d.ker) ⧸ (L ⊓ d.ker).subgroupOf (K ⊓ d.ker)) ≃
(↑(K ⊓ (L ⊔ d.ker)) ⧸ L.subgroupOf (K ⊓ (L ⊔ d.ker)))The index of L in the ker d-saturated part of K is the relative index of the corresponding kernel intersections.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relIndex_saturation_eq_inf_ker_relIndex (d : G →* D)
{L K : Subgroup G} (hLK : L ≤ K) :
L.relIndex (K ⊓ (L ⊔ d.ker)) =
(L ⊓ d.ker).relIndex (K ⊓ d.ker)The mapped relative index is the index of the ker d-saturated part of K.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem map_relIndex_eq_saturation_relIndex (d : G →* D)
(L K : Subgroup G) :
(L.map d).relIndex (K.map d) =
(K ⊓ (L ⊔ d.ker)).relIndex KThe exact relative-index identity associated to a group homomorphism.
No finite-index assumption is needed: the proof is induced by equivalences of coset types, so the equality remains valid with Mathlib's convention that an infinite relative index is 0.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relIndex_eq_map_relIndex_mul_inf_ker_relIndex (d : G →* D) {L K : Subgroup G}
(hLK : L ≤ K) :
L.relIndex K =
(L.map d).relIndex (K.map d) * (L ⊓ d.ker).relIndex (K ⊓ d.ker)The cardinality of the coset type of the intersection of two subgroups.
This is defined for arbitrary subgroups. For the cardinal relative index of an inclusion, use relativeIndexCardinal, which records the inclusion in its domain.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def intersectionIndexCardinal (L K : Subgroup G) : CardinalThe cardinality of the actual relative coset type of a subgroup inclusion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def relativeIndexCardinal {L K : Subgroup G} (_ : L ≤ K) : CardinalAt an explicitly finite boundary, the cardinal relative index specializes to Mathlib's natural-valued relative index.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relativeIndexCardinal_eq_index_of_finite {L K : Subgroup G} (hLK : L ≤ K)
[Finite (K ⧸ L.subgroupOf K)] :
relativeIndexCardinal hLK = (L.relIndex K : Cardinal)Establishes the identity relativeIndexCardinal (le_refl K) = 1.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relativeIndexCardinal_self (K : Subgroup G) :
relativeIndexCardinal (le_refl K) = 1Relative cardinal indices multiply in every subgroup tower.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relativeIndexCardinal_mul {M L K : Subgroup G}
(hML : M ≤ L) (hLK : L ≤ K) :
relativeIndexCardinal hML * relativeIndexCardinal hLK =
relativeIndexCardinal (hML.trans hLK)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def subgroupMapRestriction (d : G →* D) (K : Subgroup G) :
K →* K.map d where
toFun x := ⟨d x.1, ⟨x.1, x.2, rfl⟩⟩
map_one' := Subtype.ext (map_one d)
map_mul' x y := Subtype.ext (map_mul d x.1 y.1)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem subgroupMapRestriction_surjective (d : G →* D) (K : Subgroup G) :
Function.Surjective (subgroupMapRestriction d K)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem subgroupMapRestriction_rel_iff (d : G →* D)
(H : Subgroup D) (K : Subgroup G) (x y : K) :
QuotientGroup.leftRel ((H.comap d).subgroupOf K) x y ↔
QuotientGroup.leftRel (H.subgroupOf (K.map d))
(subgroupMapRestriction d K x) (subgroupMapRestriction d K y)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def relativeCosetComapMap (d : G →* D)
(H : Subgroup D) (K : Subgroup G) :
(K ⧸ (H.comap d).subgroupOf K) →
(K.map d ⧸ H.subgroupOf (K.map d))Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relativeCosetComapMap_injective (d : G →* D)
(H : Subgroup D) (K : Subgroup G) :
Function.Injective (relativeCosetComapMap d H K)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relativeCosetComapMap_surjective (d : G →* D)
(H : Subgroup D) (K : Subgroup G) :
Function.Surjective (relativeCosetComapMap d H K)Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def relativeCosetComapEquiv (d : G →* D)
(H : Subgroup D) (K : Subgroup G) :
(K ⧸ (H.comap d).subgroupOf K) ≃
(K.map d ⧸ H.subgroupOf (K.map d))Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]def imageCosetEquivSaturation (d : G →* D)
(L K : Subgroup G) :
(K ⧸ (K ⊓ (L ⊔ d.ker)).subgroupOf K) ≃
(K.map d ⧸ (L.map d).subgroupOf (K.map d))Cardinal form of the image contribution: it is the intersection index of the kernel-saturated part of the upper subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem intersectionIndexCardinal_image_eq_saturation (d : G →* D)
(L K : Subgroup G) :
Cardinal.lift.{u} (intersectionIndexCardinal (L.map d) (K.map d)) =
Cardinal.lift.{v}
(intersectionIndexCardinal (K ⊓ (L ⊔ d.ker)) K)Cardinal form of the kernel contribution: intersecting both subgroups with the kernel gives the saturated inner index.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relativeIndexCardinal_kernel_eq_saturation (d : G →* D)
{L K : Subgroup G} (hLK : L ≤ K) :
relativeIndexCardinal
(show L ⊓ d.ker ≤ K ⊓ d.ker from inf_le_inf hLK le_rfl) =
relativeIndexCardinal
(show L ≤ K ⊓ (L ⊔ d.ker) from fun _ hx ↦
⟨hLK hx, (show L ≤ L ⊔ d.ker from le_sup_left) hx⟩) := by
exact Cardinal.mk_congr (kernelCosetEquivSaturation d hLK)The cardinal image--kernel identity for a subgroup inclusion. It remains valid for infinite indices because it is induced by equivalences of the actual coset types.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Pointwise
universe u v
variable {G : Type u} {D : Type v} [Group G] [Group D]theorem relativeIndexCardinal_eq_map_mul_inf_ker (d : G →* D)
{L K : Subgroup G} (hLK : L ≤ K) :
Cardinal.lift.{v} (relativeIndexCardinal hLK) =
Cardinal.lift.{u}
(relativeIndexCardinal (Subgroup.map_mono (f := d) hLK)) *
Cardinal.lift.{v}
(relativeIndexCardinal
(show L ⊓ d.ker ≤ K ⊓ d.ker from inf_le_inf hLK le_rfl)) := by
have hLS : L ≤ K ⊓ (L ⊔ d.ker) := fun _ hx ↦
⟨hLK hx, (show L ≤ L ⊔ d.ker from le_sup_left) hx⟩
have hSK : K ⊓ (L ⊔ d.ker) ≤ K := inf_le_left
calc
Cardinal.lift.{v} (relativeIndexCardinal hLK) =
Cardinal.lift.{v}
(relativeIndexCardinal hLS) *
Cardinal.lift.{v}
(relativeIndexCardinal hSK) := by
rw [← Cardinal.lift_mul, relativeIndexCardinal_mul hLS hSK]
_ = Cardinal.lift.{v}
(relativeIndexCardinal
(show L ⊓ d.ker ≤ K ⊓ d.ker from inf_le_inf hLK le_rfl)) *
Cardinal.lift.{u}
(relativeIndexCardinal (Subgroup.map_mono (f := d) hLK)) := by
have hkernel :
intersectionIndexCardinal (L ⊓ d.ker) (K ⊓ d.ker) =
intersectionIndexCardinal L (K ⊓ (L ⊔ d.ker)) := by
simpa only [relativeIndexCardinal] using
relativeIndexCardinal_kernel_eq_saturation d hLK
change
Cardinal.lift.{v}
(intersectionIndexCardinal L (K ⊓ (L ⊔ d.ker))) *
Cardinal.lift.{v}
(intersectionIndexCardinal (K ⊓ (L ⊔ d.ker)) K) =
Cardinal.lift.{v}
(intersectionIndexCardinal (L ⊓ d.ker) (K ⊓ d.ker)) *
Cardinal.lift.{u}
(intersectionIndexCardinal (L.map d) (K.map d))
rw [hkernel, intersectionIndexCardinal_image_eq_saturation d L K]
_ = Cardinal.lift.{u}
(relativeIndexCardinal (Subgroup.map_mono (f := d) hLK)) *
Cardinal.lift.{v}
(relativeIndexCardinal
(show L ⊓ d.ker ≤ K ⊓ d.ker from inf_le_inf hLK le_rfl)) := mul_comm _ _