Orders along an exact sequence of groups

The order-index formula Nat.card f.ker * Nat.card f.range = Nat.card G for a group homomorphism f (Subgroup.card_ker_mul_card_range) turns exactness of a sequence of homomorphisms into identities between the orders of its terms. Along a six-term exact sequence 1 → A₀ → A₁ → A₂ → A₃ → A₄ → A₅ → 1 the alternating product of the orders is 1, written without division as |A₀| * |A₂| * |A₄| = |A₁| * |A₃| * |A₅|: at each inner node the order of the term is the product of the orders of the incoming and outgoing ranges.

The identity holds for Nat.card with no finiteness hypothesis, an infinite term contributing the factor 0 to both sides; for finite groups it is the usual statement. It is the shape a long exact cohomology sequence takes once one of its terms vanishes, and it is what turns the additivity of an Euler characteristic along a short exact sequence of coefficients into a statement about orders.

At a single node of an exact sequence A₀ → A₁ → A₂ the same count gives a divisibility |A₁| ∣ |A₀| * |A₂|, with no injectivity or surjectivity hypothesis: |A₁| is the product of the orders of the two ranges, which divide |A₀| and |A₂|. Hence A₁ is finite as soon as A₀ and A₂ are; this is recorded for bundled homomorphisms of any type, in the form in which a long exact cohomology sequence delivers it.

Main results

• MonoidHom.card_dvd_card_mul_card_of_exact: the order of the middle term of an exact sequence A₀ → A₁ → A₂ divides the product of the orders of the outer ones.
• Function.MulExact.finite, Function.Exact.finite: the middle term of an exact sequence of groups with finite outer terms is finite.
• MonoidHom.card_mul_card_mul_card_mul_card_mul_card_of_exact: the nine-term alternating identity |A₀| * |A₂| * |A₄| * |A₆| * |A₈| = |A₁| * |A₃| * |A₅| * |A₇|, the shape of a long exact cohomology sequence cut off by a vanishing H³.
• MonoidHom.card_mul_card_mul_card_of_exact: the six-term alternating identity |A₀| * |A₂| * |A₄| = |A₁| * |A₃| * |A₅|, the nine-term one padded with trivial groups.

theorem MonoidHom.card_dvd_card_mul_card_of_exact {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Group A₀] [Group A₁] [Group A₂] (f₀ : A₀ →* A₁) (f₁ : A₁ →* A₂) (h : f₀.range = f₁.ker) : Nat.card A₁ ∣ Nat.card A₀ * Nat.card A₂

The order of the middle term of an exact sequence. For an exact sequence A₀ → A₁ → A₂ of groups, |A₁| divides |A₀| * |A₂|. In particular A₁ is finite as soon as A₀ and A₂ are.

theorem AddMonoidHom.card_dvd_card_mul_card_of_exact {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [AddGroup A₀] [AddGroup A₁] [AddGroup A₂] (f₀ : A₀ →+ A₁) (f₁ : A₁ →+ A₂) (h : f₀.range = f₁.ker) : Nat.card A₁ ∣ Nat.card A₀ * Nat.card A₂

The order of the middle term of an exact sequence. For an exact sequence A₀ → A₁ → A₂ of additive groups, |A₁| divides |A₀| * |A₂|. In particular A₁ is finite as soon as A₀ and A₂ are.

theorem MonoidHom.card_mul_card_mul_card_mul_card_mul_card_of_exact {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₄ : Type u_5} {A₅ : Type u_6} {A₆ : Type u_7} {A₇ : Type u_8} {A₈ : Type u_9} [Group A₀] [Group A₁] [Group A₂] [Group A₃] [Group A₄] [Group A₅] [Group A₆] [Group A₇] [Group A₈] (f₀ : A₀ →* A₁) (f₁ : A₁ →* A₂) (f₂ : A₂ →* A₃) (f₃ : A₃ →* A₄) (f₄ : A₄ →* A₅) (f₅ : A₅ →* A₆) (f₆ : A₆ →* A₇) (f₇ : A₇ →* A₈) (h₀ : Function.Injective ⇑f₀) (h₁ : f₀.range = f₁.ker) (h₂ : f₁.range = f₂.ker) (h₃ : f₂.range = f₃.ker) (h₄ : f₃.range = f₄.ker) (h₅ : f₄.range = f₅.ker) (h₆ : f₅.range = f₆.ker) (h₇ : f₆.range = f₇.ker) (h₈ : Function.Surjective ⇑f₇) : Nat.card A₀ * Nat.card A₂ * Nat.card A₄ * Nat.card A₆ * Nat.card A₈ = Nat.card A₁ * Nat.card A₃ * Nat.card A₅ * Nat.card A₇

The alternating product of orders along a nine-term exact sequence. For an exact sequence 1 → A₀ → A₁ → ⋯ → A₇ → A₈ → 1 of groups, |A₀| * |A₂| * |A₄| * |A₆| * |A₈| = |A₁| * |A₃| * |A₅| * |A₇|.

theorem AddMonoidHom.card_mul_card_mul_card_mul_card_mul_card_of_exact {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₄ : Type u_5} {A₅ : Type u_6} {A₆ : Type u_7} {A₇ : Type u_8} {A₈ : Type u_9} [AddGroup A₀] [AddGroup A₁] [AddGroup A₂] [AddGroup A₃] [AddGroup A₄] [AddGroup A₅] [AddGroup A₆] [AddGroup A₇] [AddGroup A₈] (f₀ : A₀ →+ A₁) (f₁ : A₁ →+ A₂) (f₂ : A₂ →+ A₃) (f₃ : A₃ →+ A₄) (f₄ : A₄ →+ A₅) (f₅ : A₅ →+ A₆) (f₆ : A₆ →+ A₇) (f₇ : A₇ →+ A₈) (h₀ : Function.Injective ⇑f₀) (h₁ : f₀.range = f₁.ker) (h₂ : f₁.range = f₂.ker) (h₃ : f₂.range = f₃.ker) (h₄ : f₃.range = f₄.ker) (h₅ : f₄.range = f₅.ker) (h₆ : f₅.range = f₆.ker) (h₇ : f₆.range = f₇.ker) (h₈ : Function.Surjective ⇑f₇) : Nat.card A₀ * Nat.card A₂ * Nat.card A₄ * Nat.card A₆ * Nat.card A₈ = Nat.card A₁ * Nat.card A₃ * Nat.card A₅ * Nat.card A₇

The alternating product of orders along a nine-term exact sequence. For an exact sequence 0 → A₀ → A₁ → ⋯ → A₇ → A₈ → 0 of additive groups, |A₀| * |A₂| * |A₄| * |A₆| * |A₈| = |A₁| * |A₃| * |A₅| * |A₇|.

theorem MonoidHom.card_mul_card_mul_card_of_exact {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₄ : Type u_5} {A₅ : Type u_6} [Group A₀] [Group A₁] [Group A₂] [Group A₃] [Group A₄] [Group A₅] (f₀ : A₀ →* A₁) (f₁ : A₁ →* A₂) (f₂ : A₂ →* A₃) (f₃ : A₃ →* A₄) (f₄ : A₄ →* A₅) (h₀ : Function.Injective ⇑f₀) (h₁ : f₀.range = f₁.ker) (h₂ : f₁.range = f₂.ker) (h₃ : f₂.range = f₃.ker) (h₄ : f₃.range = f₄.ker) (h₅ : Function.Surjective ⇑f₄) : Nat.card A₀ * Nat.card A₂ * Nat.card A₄ = Nat.card A₁ * Nat.card A₃ * Nat.card A₅

The alternating product of orders along a six-term exact sequence. For an exact sequence 1 → A₀ → A₁ → A₂ → A₃ → A₄ → A₅ → 1 of groups, |A₀| * |A₂| * |A₄| = |A₁| * |A₃| * |A₅|.

theorem AddMonoidHom.card_mul_card_mul_card_of_exact {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₄ : Type u_5} {A₅ : Type u_6} [AddGroup A₀] [AddGroup A₁] [AddGroup A₂] [AddGroup A₃] [AddGroup A₄] [AddGroup A₅] (f₀ : A₀ →+ A₁) (f₁ : A₁ →+ A₂) (f₂ : A₂ →+ A₃) (f₃ : A₃ →+ A₄) (f₄ : A₄ →+ A₅) (h₀ : Function.Injective ⇑f₀) (h₁ : f₀.range = f₁.ker) (h₂ : f₁.range = f₂.ker) (h₃ : f₂.range = f₃.ker) (h₄ : f₃.range = f₄.ker) (h₅ : Function.Surjective ⇑f₄) : Nat.card A₀ * Nat.card A₂ * Nat.card A₄ = Nat.card A₁ * Nat.card A₃ * Nat.card A₅

The alternating product of orders along a six-term exact sequence. For an exact sequence 0 → A₀ → A₁ → A₂ → A₃ → A₄ → A₅ → 0 of additive groups, |A₀| * |A₂| * |A₄| = |A₁| * |A₃| * |A₅|.

theorem Function.MulExact.finite {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Group A₀] [Group A₁] [Group A₂] {F₀ : Type u_4} {F₁ : Type u_5} [FunLike F₀ A₀ A₁] [MonoidHomClass F₀ A₀ A₁] [FunLike F₁ A₁ A₂] [MonoidHomClass F₁ A₁ A₂] {f₀ : F₀} {f₁ : F₁} (h : MulExact ⇑f₀ ⇑f₁) [Finite A₀] [Finite A₂] : Finite A₁

The middle term of an exact sequence of groups with finite outer terms is finite. If A₀ → A₁ → A₂ is an exact sequence of groups and A₀, A₂ are finite, then A₁ is finite: its order divides |A₀| * |A₂|, which is nonzero.

theorem Function.Exact.finite {A₀ : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [AddGroup A₀] [AddGroup A₁] [AddGroup A₂] {F₀ : Type u_4} {F₁ : Type u_5} [FunLike F₀ A₀ A₁] [AddMonoidHomClass F₀ A₀ A₁] [FunLike F₁ A₁ A₂] [AddMonoidHomClass F₁ A₁ A₂] {f₀ : F₀} {f₁ : F₁} (h : Exact ⇑f₀ ⇑f₁) [Finite A₀] [Finite A₂] : Finite A₁

The middle term of an exact sequence of additive groups with finite outer terms is finite. If A₀ → A₁ → A₂ is an exact sequence of additive groups and A₀, A₂ are finite, then A₁ is finite: its order divides |A₀| * |A₂|, which is nonzero.