Pulling a character package back along an embedding

This module records a reusable transport principle for the topology construction. If an additive group G embeds in a group H carrying a full character package, and every prescribed limit point for an embedded injective sequence has a chosen preimage in G, then the entire package pulls back to G.

def Wallace.FullCharacterPackage.embeddedCode {G : Type u} {H : Type v} [AddCommGroup G] [AddCommGroup H] (C : FullCharacterPackage H) (e : G →+ H) (he : Function.Injective ⇑e) (s : InjectiveSequence' G) : C.Code

The code in an ambient character package corresponding to an injective sequence after it is mapped along an additive embedding.

Equations

• C.embeddedCode e he s = C.codeEquiv.symm ⟨fun (n : ℕ) => e (↑s n), ⋯⟩

def Wallace.FullCharacterPackage.pullback {G : Type u} {H : Type v} [AddCommGroup G] [AddCommGroup H] (C : FullCharacterPackage H) (e : G →+ H) (he : Function.Injective ⇑e) (limitPreimage : InjectiveSequence' G → G) (map_limitPreimage : ∀ (s : InjectiveSequence' G), e (limitPreimage s) = C.limitPoint (C.embeddedCode e he s)) : FullCharacterPackage G

Pull a full character package back along an additive embedding. The only extra datum needed is a preimage, in G, of the ambient package's prescribed limit point for every embedded injective sequence.

Equations

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

def Wallace.FullCharacterPackage.comapAddEquiv {G : Type u} {H : Type v} [AddCommGroup G] [AddCommGroup H] (C : FullCharacterPackage H) (e : G ≃+ H) : FullCharacterPackage G

Pulling a character package back along an additive equivalence requires no separate choice of limit-point preimages.

Equations

• C.comapAddEquiv e = C.pullback e.toAddMonoidHom ⋯ (fun (s : Wallace.InjectiveSequence' G) => e.symm (C.limitPoint (C.embeddedCode e.toAddMonoidHom ⋯ s))) ⋯