Conjugation actions on internal homs of discrete modules

Let a group G act on two additive monoids M and N. The additive homomorphisms M →+ N carry the conjugation action

homAction g φ : m ↦ g • φ (g⁻¹ • m),

which is the action for which evaluation (φ, m) ↦ φ m is equivariant, in the form homAction g φ (g • m) = g • φ m. This file constructs that action and proves that it is again a continuous action on a discrete module when M is finite discrete and N is discrete: the set of group elements fixing a given φ is open, and over a compact G it contains an open normal subgroup. The internal hom is contravariantly functorial in its source, by precomposition with an equivariant homomorphism, and covariantly functorial in its target, by postcomposition; Hom(-, N) is exact on the modules killed by a prime p, for every N: this is the algebra behind the dual of a short exact sequence of finite 𝔽_p[G]-modules.

Main definitions

• TauCeti.homAction: the conjugation action of G on M →+ N, with the action laws homAction_one and homAction_mul and the additivity laws homAction_zero, homAction_add, homAction_neg and homAction_sub.
• TauCeti.InternalHom: the carrier M →+ N equipped with that action, as a DistribMulAction instance. Its TauCeti.InternalHom.of and TauCeti.InternalHom.toAddMonoidHom translate to and from M →+ N.
• TauCeti.InternalHom.evalPairing: the evaluation pairing, the additive homomorphism InternalHom G M N →+ (M →+ N) whose value at φ and m is the evaluation φ m; its equivariance is TauCeti.InternalHom.evalPairing_equivariant, and that of the opposite pairing (m, φ) ↦ φ m is TauCeti.InternalHom.evalPairing_flip_equivariant.
• TauCeti.InternalHom.precomp: precomposition with an equivariant homomorphism f : M →+[G] M', the equivariant homomorphism InternalHom G M' N →+[G] InternalHom G M N, with TauCeti.InternalHom.evalPairing_precomp as its defining equation and the functor laws precomp_id and precomp_comp.
• TauCeti.InternalHom.postcomp: postcomposition with an equivariant homomorphism f : N →+[G] N', the equivariant homomorphism InternalHom G M N →+[G] InternalHom G M N', with TauCeti.InternalHom.evalPairing_postcomp as its defining equation and the functor laws postcomp_id and postcomp_comp.
• TauCeti.InternalHom.restrict: restriction of the acting group to a subgroup U ≤ G, the U-equivariant bijection InternalHom G M N →+[U] InternalHom U M N that leaves the underlying homomorphism unchanged.
• TauCeti.InternalHom.zmodEquiv: for a ZMod n-module A, evaluation at 1 identifies InternalHom G (ZMod n) A with A additively; TauCeti.InternalHom.toAddMonoidHom_apply_eq_smul recovers a homomorphism from its value at 1. For a trivial action of G on ZMod n, evaluation at 1 is equivariant (TauCeti.InternalHom.zmodEquiv_smul); for trivial actions on both M and N the conjugation action on InternalHom G M N is trivial (TauCeti.InternalHom.smul_eq_self_of_smul_eq_self).

Main results

• TauCeti.homAction_apply_smul: evaluation is equivariant; on the carrier this is TauCeti.InternalHom.evalPairing_equivariant.
• TauCeti.homAction_eq_self_iff: g fixes φ exactly when φ commutes with the action of g (TauCeti.InternalHom.smul_eq_self_iff on the carrier); so φ is fixed by all of G exactly when it is G-equivariant (TauCeti.forall_homAction_eq_self_iff, and TauCeti.InternalHom.mem_fixedPoints_iff on the carrier).
• TauCeti.isOpen_setOfPred_homAction_eq_self: for finite M and discrete N the set of group elements fixing a continuous φ is open. This is what the ContinuousSMul G instance on TauCeti.InternalHom rests on; with the discrete topology that carrier has by definition, it is what makes it again a discrete G-module for finite discrete M and discrete N.
• TauCeti.exists_openNormalSubgroup_homAction_eq_self: over a compact topological group that set contains an open normal subgroup.
• TauCeti.InternalHom.precomp_injective, TauCeti.InternalHom.exact_precomp, TauCeti.InternalHom.precomp_surjective and TauCeti.InternalHom.precomp_surjective_of_baer: Hom(-, N) takes a surjection to an injection, an exact pair with surjective second map to an exact pair, and an injection to a surjection when the target of the injection is killed by a prime p, or is killed by n with N satisfying Baer's criterion over ℤ/nℤ; both are cases of TauCeti.InternalHom.precomp_surjective_of_forall_exists_comp_eq, precomposition is surjective as soon as every additive homomorphism extends. The internal hom of finite modules is finite, and it is killed by any natural number killing the codomain (TauCeti.InternalHom.nsmul_eq_zero) or the domain (TauCeti.InternalHom.nsmul_eq_zero_of_domain).
• TauCeti.InternalHom.postcomp_injective, TauCeti.InternalHom.postcomp_bijective and TauCeti.InternalHom.postcomp_bijective_of_forall_nsmul_eq_zero: Hom(M, -) takes an injection to an injection and an isomorphism to an isomorphism, and, when M is killed by n, it takes an injection whose range is the n-torsion of its target to an isomorphism.

Implementation notes

Mathlib already puts the codomain-pointwise action (g • φ) m = g • φ m on M →+ N, as the instance in Mathlib/Algebra/GroupWithZero/Action/Hom.lean, and that action is not the conjugation one, so the conjugation action cannot be registered on M →+ N itself: instance search would be incoherent, and continuous cohomology of M →+ N would silently pick up the pointwise action. The conjugation action is therefore introduced twice over. It is first the plain function homAction of g, whose action and additivity laws are the lemmas listed above; this is the form used by the lemmas about evaluation. It is assembled from Mathlib's DistribSMul.toAddMonoidHom, which bundles each g • · as an additive homomorphism, so that its additivity comes from AddMonoidHom.comp. It is then registered as a genuine DistribMulAction on the wrapper InternalHom G M N, which is the object downstream cohomology is meant to be applied to. The two actions on M →+ N agree at any g acting trivially on the source (homAction_eq_smul_of_smul_eq_self).

The group G is a phantom parameter of InternalHom G M N: the type of its single field does not mention G, so it is formed for bare additive monoids, and Group G and the two DistribMulActions are hypotheses of the action instances only, as AddCommMonoid N is a hypothesis of the additive ones. The additive structure is transported from M →+ N along the of/toAddMonoidHom equivalence, as an AddCommMonoid in general and as an AddCommGroup when N is one. That equivalence is written inline in the two instances rather than given a name, so that the only bundled form of the carrier map in the public surface is evalPairing; the transported structure is meant to be used only through the interface lemmas below (toAddMonoidHom_zero, toAddMonoidHom_add, toAddMonoidHom_nsmul, of_zero, of_add, of_nsmul and their group-level counterparts), which hold by rfl on the transported instance.

Two theorems are instead written (rfl) rather than rfl: homAction_apply and evalPairing_apply. The module system rejects a bare rfl for an exported theorem whose proof unfolds a definition that is not @[expose]d, and those two unfold homAction and evalPairing, which nothing here needs to be exposed. The parenthesized form elaborates the same proof as an ordinary term, without that check.

Continuity in the group variable (continuous_homAction_apply) needs only that φ itself be continuous, the two actions occurring in g • φ (g⁻¹ • m) being continuous by hypothesis, and isOpen_setOfPred_homAction_eq_self inherits that hypothesis; the discrete source of the intended setting enters only where it is discharged, in the ContinuousSMul instance, by continuous_of_discreteTopology.

Representation.linHom is the same conjugation construction for k-linear maps V →ₗ[k] W of bundled representations. It is not used as the definition here for two reasons. Its carrier is V →ₗ[k] W, a type distinct from the M →+ N used for additive cochains, so routing through it would still need a bespoke definition round-tripping along AddMonoidHom.toIntLinearMap and LinearMap.toAddMonoidHom; and taking k = ℤ forces Module ℤ M and Module ℤ N, hence AddCommGroup on both sides, whereas everything below needs only AddMonoid M and AddMonoid N. In the generality where Representation.linHom is available the two constructions do agree, transported along AddMonoidHom.toIntLinearMap; that comparison is not recorded here, because it would pull Mathlib.RepresentationTheory.Basic — and with it the tensor, matrix and dual stack — into a file the whole continuous-cohomology development imports.

Mathlib puts no topology on M →+ N. Discreteness of the internal hom enters here through the discreteness of the ambient function space M → N, which is what isOpen_setOfPred_homAction_eq_self rests on. InternalHom G M N carries the discrete topology by definition, with no hypothesis on M or N: that is the intended topology in the discrete setting this file is written for, namely finite discrete M and discrete N, which is also the setting in which the action is proved continuous below. Those hypotheses are sufficient for that continuity, not necessary — if G acts trivially on both M and N then it acts trivially on M →+ N, so the action is continuous for an infinite M too — and it is sufficiency that is established here. (A trivial action on M alone does not suffice: the stabilizer of φ is then the intersection of the stabilizers of the values φ m, which for infinitely many m need not be open.) For infinite M the internal hom in the category of discrete G-modules is the sub-object of homomorphisms with open stabilizer, which is not InternalHom G M N; nothing here claims otherwise.

def TauCeti.homAction {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] (g : G) (φ : M →+ N) : M →+ N

The conjugation action of G on the internal hom M →+ N, sending φ to m ↦ g • φ (g⁻¹ • m). This is the action making evaluation equivariant; see homAction_apply_smul.

Equations

• TauCeti.homAction g φ = (DistribSMul.toAddMonoidHom N g).comp (φ.comp (DistribSMul.toAddMonoidHom M g⁻¹))

@[simp]

theorem TauCeti.homAction_apply {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] (g : G) (φ : M →+ N) (m : M) : (homAction g φ) m = g • φ (g⁻¹ • m)

@[simp]

theorem TauCeti.homAction_one {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] (φ : M →+ N) : homAction 1 φ = φ

@[simp]

theorem TauCeti.homAction_mul {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] (g h : G) (φ : M →+ N) : homAction (g * h) φ = homAction g (homAction h φ)

@[simp]

theorem TauCeti.homAction_zero {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] (g : G) : homAction g 0 = 0

@[simp]

theorem TauCeti.homAction_add {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] (g : G) (φ ψ : M →+ N) : homAction g (φ + ψ) = homAction g φ + homAction g ψ

The conjugation action is additive in the homomorphism. Of the four laws only homAction_zero holds for a bare additive-monoid codomain; this one and homAction_neg and homAction_sub all name the pointwise structure on M →+ N, hence need a commutative codomain.

@[simp]

theorem TauCeti.homAction_neg {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_4} [AddCommGroup N] [DistribMulAction G N] (g : G) (φ : M →+ N) : homAction g (-φ) = -homAction g φ

The conjugation action commutes with negation for an additive commutative codomain group.

@[simp]

theorem TauCeti.homAction_sub {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_4} [AddCommGroup N] [DistribMulAction G N] (g : G) (φ ψ : M →+ N) : homAction g (φ - ψ) = homAction g φ - homAction g ψ

The conjugation action commutes with subtraction for an additive commutative codomain group.

theorem TauCeti.homAction_apply_smul {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] (g : G) (φ : M →+ N) (m : M) : (homAction g φ) (g • m) = g • φ m

Evaluation (φ, m) ↦ φ m is equivariant for the conjugation action on M →+ N. This is the equivariance that makes the duality cup pairings well typed, and it is what fixes the direction of the conjugation action.

theorem TauCeti.homAction_eq_self_iff {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] {g : G} {φ : M →+ N} : homAction g φ = φ ↔ ∀ (m : M), φ (g • m) = g • φ m

A group element fixes φ for the conjugation action exactly when φ commutes with its action. It is deliberately not @[simp]: homAction g φ = φ is the shape in which the openness and compact-group statements below are phrased, and rewriting it away would take them out of simp-normal form.

theorem TauCeti.forall_homAction_eq_self_iff {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] {φ : M →+ N} : (∀ (g : G), homAction g φ = φ) ↔ ∀ (g : G) (m : M), φ (g • m) = g • φ m

The fixed points of the conjugation action are exactly the G-equivariant homomorphisms.

@[simp]

theorem TauCeti.homAction_id {G : Type u_1} [Group G] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] (g : G) : homAction g (AddMonoidHom.id N) = AddMonoidHom.id N

theorem TauCeti.homAction_comp {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] {P : Type u_4} [AddMonoid P] [DistribMulAction G P] (g : G) (φ : M →+ N) (ψ : N →+ P) : homAction g (ψ.comp φ) = (homAction g ψ).comp (homAction g φ)

The conjugation action is functorial for composition of homomorphisms.

theorem TauCeti.homAction_eq_smul_of_smul_eq_self {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddMonoid N] [DistribMulAction G N] {g : G} (h : ∀ (m : M), g • m = m) (φ : M →+ N) : homAction g φ = g • φ

At a group element acting trivially on the source, the conjugation action on M →+ N is Mathlib's codomain-pointwise action.

theorem TauCeti.continuous_homAction_apply {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] {M : Type u_2} [AddMonoid M] [TopologicalSpace M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type u_3} [AddMonoid N] [TopologicalSpace N] [DistribMulAction G N] [ContinuousSMul G N] {φ : M →+ N} (hφ : Continuous ⇑φ) (m : M) : Continuous fun (g : G) => (homAction g φ) m

Each value of the conjugation action is continuous in the group variable, as soon as φ itself is continuous.

theorem TauCeti.continuous_homAction_coe {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] {M : Type u_2} [AddMonoid M] [TopologicalSpace M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type u_3} [AddMonoid N] [TopologicalSpace N] [DistribMulAction G N] [ContinuousSMul G N] {φ : M →+ N} (hφ : Continuous ⇑φ) : Continuous fun (g : G) => ⇑(homAction g φ)

The conjugation action is continuous into the ambient function space M → N, as soon as φ itself is continuous.

theorem TauCeti.isOpen_setOfPred_homAction_eq_self {G : Type u_1} [Group G] [TopologicalSpace G] [ContinuousInv G] {M : Type u_2} [AddMonoid M] [TopologicalSpace M] [DistribMulAction G M] [ContinuousSMul G M] {N : Type u_3} [AddMonoid N] [TopologicalSpace N] [DistribMulAction G N] [ContinuousSMul G N] [Finite M] [DiscreteTopology N] {φ : M →+ N} (hφ : Continuous ⇑φ) : IsOpen {g : G | homAction g φ = φ}

For a finite M and a discrete N the set of group elements fixing a continuous φ is open. Discreteness enters through the ambient function space M → N; as for the two continuity lemmas above, the source only has to be discrete where Continuous φ is discharged. This is what the ContinuousSMul G (InternalHom G M N) instance below rests on, through continuousSMul_iff_stabilizer_isOpen.

structure TauCeti.InternalHom (G : Type u_1) (M : Type u_2) [AddMonoid M] (N : Type u_3) [AddMonoid N] : Type (max u_2 u_3)

The internal hom of two G-modules: the additive homomorphisms M →+ N carrying the conjugation action g • φ = homAction g φ. It is a one-field wrapper around M →+ N rather than M →+ N itself because Mathlib registers the codomain-pointwise action on the latter; this is the type on which continuous cohomology of the internal hom is to be taken. The group G is a phantom parameter, recording which action is meant. The type carries the discrete topology unconditionally, and is the internal hom of discrete G-modules in the setting this file establishes: M finite discrete and N discrete, which is sufficient for the action to be continuous.

• of :: (
• toAddMonoidHom : M →+ N

  Regard an element of the internal hom as an additive homomorphism, forgetting the action.

• )

theorem TauCeti.InternalHom.ext {G : Type u_1} {M : Type u_2} {inst✝ : AddMonoid M} {N : Type u_3} {inst✝¹ : AddMonoid N} {x y : InternalHom G M N} (toAddMonoidHom : x.toAddMonoidHom = y.toAddMonoidHom) : x = y

theorem TauCeti.InternalHom.ext_iff {G : Type u_1} {M : Type u_2} {inst✝ : AddMonoid M} {N : Type u_3} {inst✝¹ : AddMonoid N} {x y : InternalHom G M N} : x = y ↔ x.toAddMonoidHom = y.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.of_toAddMonoidHom {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] (φ : InternalHom G M N) : { toAddMonoidHom := φ.toAddMonoidHom } = φ

@[instance_reducible]

instance TauCeti.InternalHom.instTopologicalSpace {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] : TopologicalSpace (InternalHom G M N)

The internal hom always carries the discrete topology, by definition; see the implementation notes for when that is the intended topology.

Equations

• TauCeti.InternalHom.instTopologicalSpace = ⊥

instance TauCeti.InternalHom.instDiscreteTopology {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] : DiscreteTopology (InternalHom G M N)

instance TauCeti.InternalHom.instFinite {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Finite M] [Finite N] : Finite (InternalHom G M N)

The internal hom of two finite modules is finite: an additive homomorphism is determined by its underlying function.

instance TauCeti.InternalHom.instSubsingleton {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Subsingleton M] : Subsingleton (InternalHom G M N)

The internal hom out of a subsingleton module is a subsingleton: a homomorphism out of the zero module is zero.

@[instance_reducible]

instance TauCeti.InternalHom.instAddCommMonoid (G : Type u_1) {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] : AddCommMonoid (InternalHom G M N)

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.InternalHom.evalPairing (G : Type u_1) {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] : InternalHom G M N →+ M →+ N

The evaluation pairing out of the internal hom: the additive homomorphism that forgets the action, so that evalPairing G φ m is the evaluation φ m. Its equivariance is evalPairing_equivariant.

Equations

• TauCeti.InternalHom.evalPairing G = { toFun := TauCeti.InternalHom.toAddMonoidHom, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.InternalHom.evalPairing_apply {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] (φ : InternalHom G M N) : (evalPairing G) φ = φ.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_zero {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] : toAddMonoidHom 0 = 0

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_add {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] (φ ψ : InternalHom G M N) : (φ + ψ).toAddMonoidHom = φ.toAddMonoidHom + ψ.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.of_zero {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] : { toAddMonoidHom := 0 } = 0

@[simp]

theorem TauCeti.InternalHom.of_add {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] (φ ψ : M →+ N) : { toAddMonoidHom := φ + ψ } = { toAddMonoidHom := φ } + { toAddMonoidHom := ψ }

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_nsmul {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] (n : ℕ) (φ : InternalHom G M N) : (n • φ).toAddMonoidHom = n • φ.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.of_nsmul {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] (n : ℕ) (φ : M →+ N) : { toAddMonoidHom := n • φ } = n • { toAddMonoidHom := φ }

theorem TauCeti.InternalHom.nsmul_eq_zero {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] {n : ℕ} (hN : ∀ (x : N), n • x = 0) (φ : InternalHom G M N) : n • φ = 0

A natural number killing the codomain kills the internal hom.

theorem TauCeti.InternalHom.nsmul_eq_zero_of_domain {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommMonoid N] {n : ℕ} (hM : ∀ (x : M), n • x = 0) (φ : InternalHom G M N) : n • φ = 0

A natural number killing the domain kills the internal hom.

@[instance_reducible]

instance TauCeti.InternalHom.instAddCommGroup {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommGroup N] : AddCommGroup (InternalHom G M N)

For a codomain that is an additive commutative group, so is the internal hom; together with the discrete topology below this supplies coefficients for continuous cohomology.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_neg {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommGroup N] (φ : InternalHom G M N) : (-φ).toAddMonoidHom = -φ.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_sub {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommGroup N] (φ ψ : InternalHom G M N) : (φ - ψ).toAddMonoidHom = φ.toAddMonoidHom - ψ.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.of_neg {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommGroup N] (φ : M →+ N) : { toAddMonoidHom := -φ } = -{ toAddMonoidHom := φ }

@[simp]

theorem TauCeti.InternalHom.of_sub {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommGroup N] (φ ψ : M →+ N) : { toAddMonoidHom := φ - ψ } = { toAddMonoidHom := φ } - { toAddMonoidHom := ψ }

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_zsmul {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommGroup N] (z : ℤ) (φ : InternalHom G M N) : (z • φ).toAddMonoidHom = z • φ.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.of_zsmul {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_4} [AddCommGroup N] (z : ℤ) (φ : M →+ N) : { toAddMonoidHom := z • φ } = z • { toAddMonoidHom := φ }

@[instance_reducible]

instance TauCeti.InternalHom.instSMul {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] : SMul G (InternalHom G M N)

The conjugation action of G on the internal hom.

Equations

• TauCeti.InternalHom.instSMul = { smul := fun (g : G) (φ : TauCeti.InternalHom G M N) => { toAddMonoidHom := TauCeti.homAction g φ.toAddMonoidHom } }

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_smul {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] (g : G) (φ : InternalHom G M N) : (g • φ).toAddMonoidHom = homAction g φ.toAddMonoidHom

@[simp]

theorem TauCeti.InternalHom.smul_of {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] (g : G) (φ : M →+ N) : g • { toAddMonoidHom := φ } = { toAddMonoidHom := homAction g φ }

@[instance_reducible]

instance TauCeti.InternalHom.instMulAction {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] : MulAction G (InternalHom G M N)

Equations

• TauCeti.InternalHom.instMulAction = { toSMul := TauCeti.InternalHom.instSMul, mul_smul := ⋯, one_smul := ⋯ }

theorem TauCeti.InternalHom.smul_eq_self_iff {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] {g : G} {φ : InternalHom G M N} : g • φ = φ ↔ ∀ (m : M), φ.toAddMonoidHom (g • m) = g • φ.toAddMonoidHom m

A single group element fixes an element of the internal hom exactly when the underlying homomorphism commutes with its action; this is homAction_eq_self_iff on the carrier, and the form in which a stabilizer membership or an exists_openNormalSubgroup_smul_eq_self hypothesis is consumed. Like homAction_eq_self_iff it is deliberately not @[simp], since g • φ = φ is the shape in which those statements are phrased.

theorem TauCeti.InternalHom.smul_eq_self_of_smul_eq_self {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] (hM : ∀ (g : G) (m : M), g • m = m) (hN : ∀ (g : G) (x : N), g • x = x) (g : G) (φ : InternalHom G M N) : g • φ = φ

For trivial actions on M and N, the conjugation action on InternalHom G M N is trivial.

theorem TauCeti.InternalHom.mem_fixedPoints_iff {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] {φ : InternalHom G M N} : φ ∈ MulAction.fixedPoints G (InternalHom G M N) ↔ ∀ (g : G) (m : M), φ.toAddMonoidHom (g • m) = g • φ.toAddMonoidHom m

The fixed points of the internal hom are the G-equivariant homomorphisms. This is the degree-zero invariants of the conjugation action, phrased through Mathlib's MulAction.fixedPoints, which is the invariants object the surrounding development uses. It is deliberately not @[simp]: Mathlib's MulAction.mem_fixedPoints already rewrites the left-hand side, so a simp attribute here would be shadowed and the simpNF linter rejects it.

instance TauCeti.InternalHom.instContinuousSMulOfIsTopologicalGroupOfFiniteOfDiscreteTopology {G : Type u_1} {M : Type u_2} [AddMonoid M] {N : Type u_3} [AddMonoid N] [Group G] [DistribMulAction G M] [DistribMulAction G N] [TopologicalSpace G] [IsTopologicalGroup G] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul G M] [Finite M] [TopologicalSpace N] [DiscreteTopology N] [ContinuousSMul G N] : ContinuousSMul G (InternalHom G M N)

For a finite discrete M and a discrete N over a topological group, the conjugation action on the internal hom is continuous: this is the statement that InternalHom G M N is again a discrete G-module.

@[instance_reducible]

instance TauCeti.InternalHom.instDistribMulAction {G : Type u_1} {M : Type u_2} [AddMonoid M] [Group G] [DistribMulAction G M] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] : DistribMulAction G (InternalHom G M N)

Equations

• TauCeti.InternalHom.instDistribMulAction = { toMulAction := inferInstance, smul_zero := ⋯, smul_add := ⋯ }

theorem TauCeti.InternalHom.evalPairing_equivariant {G : Type u_1} {M : Type u_2} [AddMonoid M] [Group G] [DistribMulAction G M] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] (g : G) (φ : InternalHom G M N) (m : M) : ((evalPairing G) (g • φ)) (g • m) = g • ((evalPairing G) φ) m

The evaluation pairing is G-equivariant: this is the carrier form of homAction_apply_smul.

theorem TauCeti.InternalHom.evalPairing_flip_equivariant {G : Type u_1} {M : Type u_2} [AddMonoid M] [Group G] [DistribMulAction G M] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] (g : G) (m : M) (φ : InternalHom G M N) : ((evalPairing G).flip (g • m)) (g • φ) = g • ((evalPairing G).flip m) φ

The opposite evaluation pairing (m, φ) ↦ φ m is G-equivariant: evalPairing_equivariant with its two arguments swapped, in the form a cup product along the opposite pairing takes.

Contravariant functoriality in the source

def TauCeti.InternalHom.precomp (G : Type u_1) [Group G] {M : Type u_2} {M' : Type u_3} [AddMonoid M] [AddMonoid M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] (f : M →+[G] M') : InternalHom G M' N →+[G] InternalHom G M N

Precomposition with an equivariant homomorphism f : M →+[G] M', as an equivariant homomorphism InternalHom G M' N →+[G] InternalHom G M N: the internal hom is contravariantly functorial in its source. Its values are characterized by evalPairing_precomp.

Equations

• TauCeti.InternalHom.precomp G f = { toFun := fun (φ : TauCeti.InternalHom G M' N) => { toAddMonoidHom := φ.toAddMonoidHom.comp ↑f }, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_precomp {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddMonoid M] [AddMonoid M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] (f : M →+[G] M') (φ : InternalHom G M' N) : ((precomp G f) φ).toAddMonoidHom = φ.toAddMonoidHom.comp ↑f

theorem TauCeti.InternalHom.evalPairing_precomp {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddMonoid M] [AddMonoid M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] (f : M →+[G] M') (φ : InternalHom G M' N) (m : M) : ((evalPairing G) ((precomp G f) φ)) m = ((evalPairing G) φ) (f m)

Precomposition is compatible with evaluation: (φ ∘ f) m = φ (f m). Not a simp lemma, since evalPairing_apply already rewrites its left-hand side to toAddMonoidHom_precomp.

@[simp]

theorem TauCeti.InternalHom.precomp_id {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] : precomp G (DistribMulActionHom.id G) = DistribMulActionHom.id G

theorem TauCeti.InternalHom.precomp_comp {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddMonoid M] [AddMonoid M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] {M'' : Type u_5} [AddMonoid M''] [DistribMulAction G M''] (g : M' →+[G] M'') (f : M →+[G] M') : precomp G (g.comp f) = (precomp G f).comp (precomp G g)

theorem TauCeti.InternalHom.precomp_injective {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddMonoid M] [AddMonoid M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] {f : M →+[G] M'} (hf : Function.Surjective ⇑f) : Function.Injective ⇑(precomp G f)

Precomposition with a surjection is injective: Hom(-, N) takes surjections to injections.

theorem TauCeti.InternalHom.precomp_surjective_of_forall_exists_comp_eq {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddMonoid M] [AddMonoid M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] {f : M →+[G] M'} (h : ∀ (φ : M →+ N), ∃ (ψ : M' →+ N), ψ.comp ↑f = φ) : Function.Surjective ⇑(precomp G f)

Precomposition with f is surjective on internal homs as soon as every additive homomorphism M →+ N is the restriction along f of an additive homomorphism M' →+ N: the extension, with the conjugation action, is a preimage in the internal hom.

theorem TauCeti.InternalHom.precomp_bijective {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddMonoid M] [AddMonoid M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] {f : M →+[G] M'} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(precomp G f)

Precomposition with a bijection is bijective: Hom(-, N) takes isomorphisms to isomorphisms. The inverse is precomposition with the inverse bijection.

Covariant functoriality in the target

def TauCeti.InternalHom.postcomp (G : Type u_1) [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} {N' : Type u_4} [AddCommMonoid N] [AddCommMonoid N'] [DistribMulAction G N] [DistribMulAction G N'] (f : N →+[G] N') : InternalHom G M N →+[G] InternalHom G M N'

Postcomposition with an equivariant homomorphism f : N →+[G] N', as an equivariant homomorphism InternalHom G M N →+[G] InternalHom G M N': the internal hom is covariantly functorial in its target. Its values are characterized by evalPairing_postcomp.

Equations

• TauCeti.InternalHom.postcomp G f = { toFun := fun (φ : TauCeti.InternalHom G M N) => { toAddMonoidHom := (↑f).comp φ.toAddMonoidHom }, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_postcomp {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} {N' : Type u_4} [AddCommMonoid N] [AddCommMonoid N'] [DistribMulAction G N] [DistribMulAction G N'] (f : N →+[G] N') (φ : InternalHom G M N) : ((postcomp G f) φ).toAddMonoidHom = (↑f).comp φ.toAddMonoidHom

theorem TauCeti.InternalHom.evalPairing_postcomp {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} {N' : Type u_4} [AddCommMonoid N] [AddCommMonoid N'] [DistribMulAction G N] [DistribMulAction G N'] (f : N →+[G] N') (φ : InternalHom G M N) (m : M) : ((evalPairing G) ((postcomp G f) φ)) m = f (((evalPairing G) φ) m)

Postcomposition is compatible with evaluation: (f ∘ φ) m = f (φ m). Not a simp lemma, since evalPairing_apply already rewrites its left-hand side to toAddMonoidHom_postcomp.

@[simp]

theorem TauCeti.InternalHom.postcomp_id {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] : postcomp G (DistribMulActionHom.id G) = DistribMulActionHom.id G

theorem TauCeti.InternalHom.postcomp_comp {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} {N' : Type u_4} [AddCommMonoid N] [AddCommMonoid N'] [DistribMulAction G N] [DistribMulAction G N'] {N'' : Type u_5} [AddCommMonoid N''] [DistribMulAction G N''] (g : N' →+[G] N'') (f : N →+[G] N') : postcomp G (g.comp f) = (postcomp G g).comp (postcomp G f)

theorem TauCeti.InternalHom.postcomp_injective {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} {N' : Type u_4} [AddCommMonoid N] [AddCommMonoid N'] [DistribMulAction G N] [DistribMulAction G N'] {f : N →+[G] N'} (hf : Function.Injective ⇑f) : Function.Injective ⇑(postcomp G f)

Postcomposition with an injection is injective: Hom(M, -) takes injections to injections.

theorem TauCeti.InternalHom.postcomp_bijective_of_forall_nsmul_eq_zero {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} {N' : Type u_4} [AddCommMonoid N] [AddCommMonoid N'] [DistribMulAction G N] [DistribMulAction G N'] {f : N →+[G] N'} (hf : Function.Injective ⇑f) {n : ℕ} (hM : ∀ (x : M), n • x = 0) (hN' : ∀ (y : N'), n • y = 0 → ∃ (x : N), f x = y) : Function.Bijective ⇑(postcomp G f)

Postcomposition with an injection onto the n-torsion is bijective on the internal homs out of a module killed by n: if f : N →+[G] N' is injective and every element of N' killed by n lies in its range, then Hom(M, f) is bijective for every M killed by n, because every homomorphism out of M takes values in the n-torsion.

theorem TauCeti.InternalHom.postcomp_bijective {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} {N' : Type u_4} [AddCommMonoid N] [AddCommMonoid N'] [DistribMulAction G N] [DistribMulAction G N'] {f : N →+[G] N'} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(postcomp G f)

Postcomposition with a bijection is bijective: Hom(M, -) takes isomorphisms to isomorphisms. This is the case n = 0 of postcomp_bijective_of_forall_nsmul_eq_zero.

Restricting the acting group

def TauCeti.InternalHom.restrict {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] (U : Subgroup G) : InternalHom G M N →+[↥U] InternalHom (↥U) M N

Restricting the acting group to a subgroup U ≤ G: the internal hom of M and N as G-modules, regarded as a U-module through the restricted action, is the internal hom of M and N as U-modules. The underlying homomorphism does not move (toAddMonoidHom_restrict), the evaluation pairing is unchanged (evalPairing_restrict) and the map is a bijection (restrict_bijective). It is recorded as a U-equivariant homomorphism because that is the form in which the coefficient maps of continuous cohomology consume it.

Equations

• TauCeti.InternalHom.restrict U = { toFun := fun (φ : TauCeti.InternalHom G M N) => { toAddMonoidHom := φ.toAddMonoidHom }, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_restrict {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] (U : Subgroup G) (φ : InternalHom G M N) : ((restrict U) φ).toAddMonoidHom = φ.toAddMonoidHom

theorem TauCeti.InternalHom.evalPairing_restrict {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] (U : Subgroup G) (φ : InternalHom G M N) (m : M) : ((evalPairing ↥U) ((restrict U) φ)) m = ((evalPairing G) φ) m

Restricting the acting group does not change the evaluation pairing.

theorem TauCeti.InternalHom.restrict_bijective {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] (U : Subgroup G) : Function.Bijective ⇑(restrict U)

theorem TauCeti.InternalHom.exact_precomp {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} {M'' : Type u_4} [AddMonoid M] [AddGroup M'] [AddGroup M''] [DistribMulAction G M] [DistribMulAction G M'] [DistribMulAction G M''] {N : Type u_5} [AddCommGroup N] [DistribMulAction G N] (f : M →+[G] M') (g : M' →+[G] M'') (hg : Function.Surjective ⇑g) (hfg : Function.Exact ⇑f ⇑g) : Function.Exact ⇑(precomp G g) ⇑(precomp G f)

Precomposition along an exact pair f : M →+[G] M', g : M' →+[G] M'' with g surjective is exact: a homomorphism on M' killing the image of f factors through g. The groups M' and M'' need not be commutative.

theorem TauCeti.InternalHom.precomp_surjective {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddCommGroup M] [AddCommGroup M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommMonoid N] [DistribMulAction G N] {p : ℕ} [Fact (Nat.Prime p)] (hM' : ∀ (x : M'), p • x = 0) {f : M →+[G] M'} (hf : Function.Injective ⇑f) : Function.Surjective ⇑(precomp G f)

Precomposition with an injection into a module killed by a prime p is surjective, for any N: Hom(-, N) is exact on the modules killed by p. This is AddMonoidHom.exists_comp_eq_of_injective on the internal hom.

theorem TauCeti.InternalHom.precomp_surjective_of_baer {G : Type u_1} [Group G] {M : Type u_2} {M' : Type u_3} [AddCommGroup M] [AddCommGroup M'] [DistribMulAction G M] [DistribMulAction G M'] {N : Type u_4} [AddCommGroup N] [DistribMulAction G N] {n : ℕ} [Module (ZMod n) N] (hN : Module.Baer (ZMod n) N) (hM' : ∀ (x : M'), n • x = 0) {f : M →+[G] M'} (hf : Function.Injective ⇑f) : Function.Surjective ⇑(precomp G f)

Precomposition with an injection into a module killed by n is surjective when the target N satisfies Baer's criterion over ℤ/nℤ: for such N, Hom(-, N) is exact on the modules killed by n. This holds for N = ℤ/nℤ with any action when n ≠ 0, by Module.Baer.zmod_self, and is AddMonoidHom.exists_comp_eq_of_injective_of_baer on the internal hom.

theorem TauCeti.exists_openNormalSubgroup_homAction_eq_self {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {M : Type u_2} [AddMonoid M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [Finite M] {N : Type u_3} [AddMonoid N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (φ : M →+ N) : ∃ (U : OpenNormalSubgroup G), ∀ u ∈ U, homAction u φ = φ

Over a compact topological group, a homomorphism from a finite discrete module to a discrete module is fixed by an open normal subgroup. This is the form used by the finite-quotient system for continuous cohomology. It is exists_openNormalSubgroup_smul_eq_self for the discrete G-module InternalHom G M N, read back on M →+ N.

Homomorphisms out of ZMod n

An additive homomorphism out of ZMod n is determined by its value at 1, so the internal hom InternalHom G (ZMod n) A is additively A itself whenever A is a ZMod n-module. The action of G plays no part in this identification.

theorem TauCeti.InternalHom.toAddMonoidHom_apply_eq_smul (G : Type u_1) {n : ℕ} {A : Type u_2} [AddCommGroup A] [Module (ZMod n) A] (φ : InternalHom G (ZMod n) A) (x : ZMod n) : φ.toAddMonoidHom x = x • φ.toAddMonoidHom 1

A homomorphism out of ZMod n into a ZMod n-module is scalar multiplication by its value at 1: it is ZMod n-linear, and x = x • 1.

def TauCeti.InternalHom.zmodEquiv (G : Type u_1) {n : ℕ} {A : Type u_2} [AddCommGroup A] [Module (ZMod n) A] : InternalHom G (ZMod n) A ≃+ A

Homomorphisms out of ZMod n are elements. For a ZMod n-module A, evaluation at 1 identifies the internal hom InternalHom G (ZMod n) A with A, additively; the inverse sends a to x ↦ x • a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.InternalHom.zmodEquiv_apply (G : Type u_1) {n : ℕ} {A : Type u_2} [AddCommGroup A] [Module (ZMod n) A] (φ : InternalHom G (ZMod n) A) : (zmodEquiv G) φ = φ.toAddMonoidHom 1

@[simp]

theorem TauCeti.InternalHom.zmodEquiv_symm_apply (G : Type u_1) {n : ℕ} {A : Type u_2} [AddCommGroup A] [Module (ZMod n) A] (a : A) (x : ZMod n) : ((zmodEquiv G).symm a).toAddMonoidHom x = x • a

theorem TauCeti.InternalHom.zmodEquiv_smul {G : Type u_1} {n : ℕ} {A : Type u_2} [AddCommGroup A] [Module (ZMod n) A] [Group G] [DistribMulAction G (ZMod n)] [DistribMulAction G A] (htriv : ∀ (g : G) (m : ZMod n), g • m = m) (g : G) (φ : InternalHom G (ZMod n) A) : (zmodEquiv G) (g • φ) = g • (zmodEquiv G) φ

For a trivial action on the source ZMod n, evaluation at 1 is G-equivariant for the conjugation action on InternalHom G (ZMod n) A and any action on A: (g • φ) 1 = g • φ 1, since g⁻¹ • 1 = 1.