A nonempty fiber of a group homomorphism is a copy of the kernel

A nonempty fiber of f is a coset of ker f. Mathlib's AddMonoidHom.fiberEquivKer says this in the set-preimage form f ⁻¹' {f a}, with the attained value written as a value of f, and over an additive group. A caller usually meets the fiber as the subtype {a // f a = b} instead and holds f a = b separately, and a kernel asks only AddZeroClass of the codomain, so subtypeFiberEquivKer is built here at that generality: x ↦ -a + x, with a + · back. Four consequences follow from it: the fiber is counted, made finite, and a sum over it is reindexed as a sum over the kernel; and summing g ∘ f along a surjective f counts each value of g as often as the kernel has elements.

Finiteness is the one of the four that needs no preimage: an empty fiber is finite as well, so the statement is available before any point of the fiber is known, which is what a caller quantifying over all values of f wants.

The multiplication map n • · of an additive commutative group is the case the counting arguments for isogenies use: each of its nonempty fibers has as many elements as the n-torsion. Emptiness is not excluded by fiat — n • · need not be surjective. The cardinality and reindexing results therefore take a point in the fiber as an argument, while the finiteness result does not.

Main results

• AddMonoidHom.subtypeFiberEquivKer (and MonoidHom.subtypeFiberEquivKer): the fiber over an attained value, as a subtype, is equivalent to the kernel, translating by -a and its inverse by a.
• AddMonoidHom.card_fiber_eq_card_ker (and MonoidHom.card_fiber_eq_card_ker): a nonempty fiber has as many elements as the kernel.
• AddMonoidHom.finite_fiber (and MonoidHom.finite_fiber): every fiber is finite when the kernel is.
• AddMonoidHom.sum_fiber_eq_sum_ker_add_left (and MonoidHom.prod_fiber_eq_prod_ker_mul_left): summing an arbitrary function over a nonempty fiber is summing its values on a + t over the kernel.
• AddMonoidHom.sum_comp_of_surjective (and MonoidHom.prod_comp_of_surjective): summing g ∘ f along a surjective homomorphism counts each value of g as often as the kernel.
• TauCeti.card_zsmul_fiber_eq_card_zsmul_eq_zero: the same for n • · on an additive commutative group, with the kernel written as the n-torsion.

Provenance

Generalized from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0) pinned at a302aeacd86053f9d5f991fbbf664e1cc1051d08: HasseWeil/HasseBound/WeilPairing/Fiber.lean, declarations fiberEquivKer, fiber_finite and fiber_card_eq_ker_card, and HasseWeil/HasseBound/WeilPairing/SigmaBridge.lean, declaration fiber_sum_eq_ker_sum. There they are stated for an endomorphism of the point group of an elliptic curve; here they hold of any homomorphism of groups, the commutative hypothesis appearing only where an unordered product is taken. Like the source, the equivalence is built directly: Mathlib's fiberEquivKer requires a group codomain, while this version only needs MulOneClass (additively, AddZeroClass). On the overlap the two equivalences use the same translations.

def MonoidHom.subtypeFiberEquivKer {G : Type u_1} {H : Type u_2} [Group G] [MulOneClass H] (f : G →* H) {b : H} {a : G} (ha : f a = b) : { x : G // f x = b } ≃ ↥f.ker

A nonempty fiber is a copy of the kernel, in the subtype form: given ha : f a = b, the fiber over b is a times the kernel. Mathlib's MonoidHom.fiberEquivKer is the same map at [Group H], stated on the set preimage f ⁻¹' {f a}; the codomain of a kernel needs only MulOneClass, which is where this is built.

Equations

• f.subtypeFiberEquivKer ha = { toFun := fun (x : { x : G // f x = b }) => ⟨a⁻¹ * ↑x, ⋯⟩, invFun := fun (t : ↥f.ker) => ⟨a * ↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

def AddMonoidHom.subtypeFiberEquivKer {G : Type u_1} {H : Type u_2} [AddGroup G] [AddZeroClass H] (f : G →+ H) {b : H} {a : G} (ha : f a = b) : { x : G // f x = b } ≃ ↥f.ker

A nonempty fiber is a copy of the kernel, in the subtype form: given ha : f a = b, the fiber over b is a plus the kernel. Mathlib's AddMonoidHom.fiberEquivKer is the same map at [AddGroup H], stated on the set preimage f ⁻¹' {f a}; the codomain of a kernel needs only AddZeroClass, which is where this is built.

Equations

• f.subtypeFiberEquivKer ha = { toFun := fun (x : { x : G // f x = b }) => ⟨-a + ↑x, ⋯⟩, invFun := fun (t : ↥f.ker) => ⟨a + ↑t, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MonoidHom.subtypeFiberEquivKer_apply {G : Type u_1} {H : Type u_2} [Group G] [MulOneClass H] (f : G →* H) {b : H} {a : G} (ha : f a = b) (x : { x : G // f x = b }) : ↑((f.subtypeFiberEquivKer ha) x) = a⁻¹ * ↑x

The equivalence translates by a⁻¹.

@[simp]

theorem AddMonoidHom.subtypeFiberEquivKer_apply {G : Type u_1} {H : Type u_2} [AddGroup G] [AddZeroClass H] (f : G →+ H) {b : H} {a : G} (ha : f a = b) (x : { x : G // f x = b }) : ↑((f.subtypeFiberEquivKer ha) x) = -a + ↑x

The equivalence translates by -a.

@[simp]

theorem MonoidHom.subtypeFiberEquivKer_symm_apply {G : Type u_1} {H : Type u_2} [Group G] [MulOneClass H] (f : G →* H) {b : H} {a : G} (ha : f a = b) (t : ↥f.ker) : ↑((f.subtypeFiberEquivKer ha).symm t) = a * ↑t

Its inverse translates by a.

@[simp]

theorem AddMonoidHom.subtypeFiberEquivKer_symm_apply {G : Type u_1} {H : Type u_2} [AddGroup G] [AddZeroClass H] (f : G →+ H) {b : H} {a : G} (ha : f a = b) (t : ↥f.ker) : ↑((f.subtypeFiberEquivKer ha).symm t) = a + ↑t

Its inverse translates by a.

theorem MonoidHom.card_fiber_eq_card_ker {G : Type u_1} {H : Type u_2} [Group G] [MulOneClass H] (f : G →* H) {b : H} {a : G} (ha : f a = b) : Nat.card { x : G // f x = b } = Nat.card ↥f.ker

A nonempty fiber has as many elements as the kernel.

theorem AddMonoidHom.card_fiber_eq_card_ker {G : Type u_1} {H : Type u_2} [AddGroup G] [AddZeroClass H] (f : G →+ H) {b : H} {a : G} (ha : f a = b) : Nat.card { x : G // f x = b } = Nat.card ↥f.ker

A nonempty fiber has as many elements as the kernel.

theorem MonoidHom.finite_fiber {G : Type u_1} {H : Type u_2} [Group G] [MulOneClass H] (f : G →* H) [Finite ↥f.ker] (b : H) : Finite { x : G // f x = b }

Every fiber is finite when the kernel is. The empty fiber is covered too, so no preimage has to be produced first.

theorem AddMonoidHom.finite_fiber {G : Type u_1} {H : Type u_2} [AddGroup G] [AddZeroClass H] (f : G →+ H) [Finite ↥f.ker] (b : H) : Finite { x : G // f x = b }

Every fiber is finite when the kernel is. The empty fiber is covered too, so no preimage has to be produced first.

theorem MonoidHom.prod_fiber_eq_prod_ker_mul_left {G : Type u_1} {H : Type u_2} {M : Type u_3} [Group G] [MulOneClass H] [CommMonoid M] (f : G →* H) {b : H} {a : G} (ha : f a = b) [Fintype { x : G // f x = b }] [Fintype ↥f.ker] (g : G → M) : ∏ x : { x : G // f x = b }, g ↑x = ∏ t : ↥f.ker, g (a * ↑t)

A product over a nonempty fiber is a product over the kernel translated on the left. For a chosen point a in the fiber over b, the product of g over the fiber equals the product of g (a * t) over the kernel. Both Fintype instances are supplied by the caller.

theorem AddMonoidHom.sum_fiber_eq_sum_ker_add_left {G : Type u_1} {H : Type u_2} {M : Type u_3} [AddGroup G] [AddZeroClass H] [AddCommMonoid M] (f : G →+ H) {b : H} {a : G} (ha : f a = b) [Fintype { x : G // f x = b }] [Fintype ↥f.ker] (g : G → M) : ∑ x : { x : G // f x = b }, g ↑x = ∑ t : ↥f.ker, g (a + ↑t)

A sum over a nonempty fiber is a sum over the kernel translated on the left. For a chosen point a in the fiber over b, the sum of g over the fiber equals the sum of g (a + t) over the kernel. Both Fintype instances are supplied by the caller.

theorem MonoidHom.prod_comp_of_surjective {G : Type u_1} {H : Type u_2} {M : Type u_3} [Group G] [MulOneClass H] [CommMonoid M] [Fintype G] [Fintype H] (f : G →* H) (hf : Function.Surjective ⇑f) (g : H → M) : ∏ x : G, g (f x) = (∏ y : H, g y) ^ Nat.card ↥f.ker

A product along a surjective homomorphism. Every fiber of a surjective f is a copy of its kernel, so the product of g ∘ f over G is the product of g over H, raised to the order of the kernel.

theorem AddMonoidHom.sum_comp_of_surjective {G : Type u_1} {H : Type u_2} {M : Type u_3} [AddGroup G] [AddZeroClass H] [AddCommMonoid M] [Fintype G] [Fintype H] (f : G →+ H) (hf : Function.Surjective ⇑f) (g : H → M) : ∑ x : G, g (f x) = Nat.card ↥f.ker • ∑ y : H, g y

A sum along a surjective homomorphism. Every fiber of a surjective f is a copy of its kernel, so the sum of g ∘ f over G is the order of the kernel times the sum of g over H.

theorem TauCeti.card_zsmul_fiber_eq_card_zsmul_eq_zero {G : Type u_1} [AddCommGroup G] {n : ℤ} {T P₀ : G} (hP₀ : n • P₀ = T) : Nat.card { P : G // n • P = T } = Nat.card { P : G // n • P = 0 }

A nonempty fiber of n • · has as many elements as the n-torsion.