Semilinear functoriality of Kähler differentials along algebra homomorphisms

For an R-algebra homomorphism f : A →ₐ[R] B, the induced map on Kähler differentials sends D x to D (f x). It is R-linear, since f fixes R, but it moves the A-action through f — it is f-semilinear, mapSemilinear f (a • ω) = f a • mapSemilinear f ω — so it is packaged as a semilinear map Ω[A⁄R] →ₛₗ[f.toRingHom] Ω[B⁄R], following the precedent of LinearMap.frobenius. The motivating special case is an algebra endomorphism f : S →ₐ[R] S (for instance Frobenius), where this is the pullback of differentials along f and where the map need not be S-linear.

Mathlib's KaehlerDifferential.map is functoriality for a tower [Algebra A B] [IsScalarTower R A B], so it cannot state this map: for an arbitrary f : A →ₐ[R] B no Algebra A B instance exists, and for an endomorphism, installing one would clash with Algebra.id. The two structures induced by f do exist locally, however, and mapSemilinear is KaehlerDifferential.map under those local letI instances, repackaged with the A-action on the target unfolded into f-semilinearity — which is exactly the statement that survives outside the letI scope.

Main definitions

• KaehlerDifferential.mapSemilinear f : Ω[A⁄R] →ₛₗ[f.toRingHom] Ω[B⁄R]

Main results

• KaehlerDifferential.mapSemilinear_D: mapSemilinear f (D x) = D (f x). This characterises the map: Ω[A⁄R] is spanned by the range of D (span_range_derivation), so two semilinear maps agreeing there are equal by LinearMap.ext_on.
• KaehlerDifferential.mapSemilinear_toAlgHom_apply: on a tower it agrees with Mathlib's KaehlerDifferential.map.
• KaehlerDifferential.mapSemilinear_smul: the semilinearity law, with f applied rather than f.toRingHom.
• KaehlerDifferential.mapSemilinear_id, mapSemilinear_id_apply: the identity acts as the identity.
• KaehlerDifferential.mapSemilinear_comp_apply, mapSemilinear_comp: compatibility with composition.

Provenance

Ported from the AINTLIB HasseWeil project (Apache-2.0), revision 513e83879e2f, file HasseWeil/Auxiliary/PullbackKaehler.lean, declarations AlgHom.pullbackKaehler, pullbackKaehler_D, pullbackKaehler_smul_R, pullbackKaehler_smul_S, pullbackKaehler_comp and pullbackKaehler_id. The source treats an endomorphism of a fixed S, exports an AddMonoidHom with hand-stated semilinearity lemmas, and builds the map from scratch through a public TwistedKaehler module; here the map is generalised to an arbitrary R-algebra homomorphism A →ₐ[R] B, constructed from Mathlib's KaehlerDifferential.map, and exported as the semilinear map, whose type already carries the scalar law the source stated by hand.

noncomputable def KaehlerDifferential.mapSemilinear {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : Ω[A⁄R] →ₛₗ[f.toRingHom] Ω[B⁄R]

The map of Kähler differentials along an R-algebra homomorphism f : A →ₐ[R] B, characterised by mapSemilinear f (D x) = D (f x). It is f-semilinear: mapSemilinear f (a • ω) = f a • mapSemilinear f ω (mapSemilinear_smul).

This is KaehlerDifferential.map under the local Algebra A B structure induced by f, repackaged semilinearly so that the statement survives outside that instance's scope.

Equations

• KaehlerDifferential.mapSemilinear f = { toFun := ⇑(KaehlerDifferential.map R R A B), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem KaehlerDifferential.mapSemilinear_D {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (x : A) : (mapSemilinear f) ((D R A) x) = (D R B) (f x)

mapSemilinear f sends D x to D (f x).

@[simp]

theorem KaehlerDifferential.mapSemilinear_smul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (a : A) (ω : Ω[A⁄R]) : (mapSemilinear f) (a • ω) = f a • (mapSemilinear f) ω

The semilinearity law of mapSemilinear, stated with f applied rather than f.toRingHom.

This is not interchangeable with the generic map_smulₛₗ: that lemma produces the coefficient f.toRingHom a, which is only definitionally f a, and it carries no @[simp] attribute, so simp alone leaves mapSemilinear f (a • ω) untouched. This is the simp-normal form.

theorem KaehlerDifferential.mapSemilinear_id {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] : mapSemilinear (AlgHom.id R A) = LinearMap.id

The map along the identity is the identity, as (plainly linear) maps.

@[simp]

theorem KaehlerDifferential.mapSemilinear_id_apply {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (ω : Ω[A⁄R]) : (mapSemilinear (AlgHom.id R A)) ω = ω

The map along the identity fixes every differential.

theorem KaehlerDifferential.mapSemilinear_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) : mapSemilinear (f.comp g) = mapSemilinear f ∘ₛₗ mapSemilinear g

Functoriality of mapSemilinear, at map level.

@[simp]

theorem KaehlerDifferential.mapSemilinear_comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [CommRing B] [CommRing C] [Algebra R A] [Algebra R B] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) (ω : Ω[A⁄R]) : (mapSemilinear (f.comp g)) ω = (mapSemilinear f) ((mapSemilinear g) ω)

mapSemilinear is functorial: mapping along f.comp g is mapping along g, then along f.

@[simp]

theorem KaehlerDifferential.mapSemilinear_toAlgHom_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B] (ω : Ω[A⁄R]) : (mapSemilinear (IsScalarTower.toAlgHom R A B)) ω = (map R R A B) ω

On a tower, mapSemilinear along the structure map is Mathlib's KaehlerDifferential.map — the sense in which this construction extends the tower functoriality to arbitrary algebra homomorphisms.