The module of kaehler differentials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main results #
kaehler_differential: The module of kaehler differentials. For anR-algebraS, we provide the notationΩ[S⁄R]forkaehler_differential R S. Note that the slash is\textfractionsolidus.kaehler_differential.D: The derivation into the module of kaehler differentials.kaehler_differential.span_range_derivation: The image ofDspansΩ[S⁄R]as anS-module.kaehler_differential.linear_map_equiv_derivation: The isomorphismHom_R(Ω[S⁄R], M) ≃ₗ[S] Der_R(S, M).kaehler_differential.quot_ker_total_equiv: An alternative description ofΩ[S⁄R]asScopies ofSwith kernel (kaehler_differential.ker_total) generated by the relations:dx + dy = d(x + y)x dy + y dx = d(x * y)dr = 0forr ∈ R
kaehler_differential.map: Given a map between the arrowsR → AandS → B, we have anA-linear mapΩ[A⁄R] → Ω[B⁄S].
Future project #
- Define a
is_kaehler_differentialpredicate.
@[reducible]
def
kaehler_differential.ideal
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
ideal (tensor_product R S S)
The kernel of the multiplication map S ⊗[R] S →ₐ[R] S.
def
derivation.tensor_product_to
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(D : derivation R S M) :
tensor_product R S S →ₗ[S] M
For a R-derivation S → M, this is the map S ⊗[R] S →ₗ[S] M sending s ⊗ₜ t ↦ s • D t.
Equations
- D.tensor_product_to = tensor_product.algebra_tensor_module.lift (⇑((linear_map.lsmul S (S →ₗ[R] M)).flip) D.to_linear_map)
theorem
derivation.tensor_product_to_tmul
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(D : derivation R S M)
(s t : S) :
theorem
derivation.tensor_product_to_mul
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(D : derivation R S M)
(x y : tensor_product R S S) :
⇑(D.tensor_product_to) (x * y) = ⇑(algebra.tensor_product.lmul' R) x • ⇑(D.tensor_product_to) y + ⇑(algebra.tensor_product.lmul' R) y • ⇑(D.tensor_product_to) x
theorem
kaehler_differential.submodule_span_range_eq_ideal
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
submodule.span S (set.range (λ (s : S), 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)) = submodule.restrict_scalars S (kaehler_differential.ideal R S)
The kernel of S ⊗[R] S →ₐ[R] S is generated by 1 ⊗ s - s ⊗ 1 as a S-module.
def
kaehler_differential
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
Type u_2
The module of Kähler differentials (Kahler differentials, Kaehler differentials).
This is implemented as I / I ^ 2 with I the kernel of the multiplication map S ⊗[R] S →ₐ[R] S.
To view elements as a linear combination of the form s • D s', use
kaehler_differential.tensor_product_to_surjective and derivation.tensor_product_to_tmul.
We also provide the notation Ω[S⁄R] for kaehler_differential R S.
Note that the slash is \textfractionsolidus.
Instances for kaehler_differential
- kaehler_differential.add_comm_group
- kaehler_differential.module
- kaehler_differential.nonempty
- kaehler_differential.module'
- kaehler_differential.is_scalar_tower
- kaehler_differential.is_scalar_tower_of_tower
- kaehler_differential.is_scalar_tower'
- algebra.formally_unramified.subsingleton_kaehler_differential
@[protected, instance]
def
kaehler_differential.module'
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
{R' : Type u_3}
[comm_ring R']
[algebra R' S]
[smul_comm_class R R' S] :
Equations
@[protected, instance]
def
kaehler_differential.is_scalar_tower
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
is_scalar_tower S (tensor_product R S S) Ω[S⁄R]
@[protected, instance]
def
kaehler_differential.is_scalar_tower_of_tower
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
{R₁ : Type u_3}
{R₂ : Type u_4}
[comm_ring R₁]
[comm_ring R₂]
[algebra R₁ S]
[algebra R₂ S]
[has_smul R₁ R₂]
[smul_comm_class R R₁ S]
[smul_comm_class R R₂ S]
[is_scalar_tower R₁ R₂ S] :
is_scalar_tower R₁ R₂ Ω[S⁄R]
@[protected, instance]
def
kaehler_differential.is_scalar_tower'
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
is_scalar_tower R (tensor_product R S S) Ω[S⁄R]
def
kaehler_differential.from_ideal
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
↥(kaehler_differential.ideal R S) →ₗ[tensor_product R S S] Ω[S⁄R]
The quotient map I → Ω[S⁄R] with I being the kernel of S ⊗[R] S → S.
Equations
def
kaehler_differential.D_linear_map
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
(Implementation) The underlying linear map of the derivation into Ω[S⁄R].
Equations
- kaehler_differential.D_linear_map R S = (linear_map.restrict_scalars R (kaehler_differential.from_ideal R S)).comp (linear_map.cod_restrict (submodule.restrict_scalars R (kaehler_differential.ideal R S)) (algebra.tensor_product.include_right.to_linear_map - algebra.tensor_product.include_left.to_linear_map) _)
theorem
kaehler_differential.D_linear_map_apply
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(s : S) :
⇑(kaehler_differential.D_linear_map R S) s = ⇑((kaehler_differential.ideal R S).to_cotangent) ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, _⟩
def
kaehler_differential.D
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
derivation R S Ω[S⁄R]
The universal derivation into Ω[S⁄R].
Equations
- kaehler_differential.D R S = {to_linear_map := kaehler_differential.D_linear_map R S _inst_3, map_one_eq_zero' := _, leibniz' := _}
theorem
kaehler_differential.D_apply
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(s : S) :
⇑(kaehler_differential.D R S) s = ⇑((kaehler_differential.ideal R S).to_cotangent) ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, _⟩
theorem
kaehler_differential.span_range_derivation
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
submodule.span S (set.range ⇑(kaehler_differential.D R S)) = ⊤
def
derivation.lift_kaehler_differential
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(D : derivation R S M) :
The linear map from Ω[S⁄R], associated with a derivation.
Equations
theorem
derivation.lift_kaehler_differential_apply
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(D : derivation R S M)
(x : ↥(kaehler_differential.ideal R S)) :
⇑(D.lift_kaehler_differential) (⇑((kaehler_differential.ideal R S).to_cotangent) x) = ⇑(D.tensor_product_to) ↑x
theorem
derivation.lift_kaehler_differential_comp
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(D : derivation R S M) :
⇑(D.lift_kaehler_differential.comp_der) (kaehler_differential.D R S) = D
@[simp]
theorem
derivation.lift_kaehler_differential_comp_D
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(D' : derivation R S M)
(x : S) :
⇑(D'.lift_kaehler_differential) (⇑(kaehler_differential.D R S) x) = ⇑D' x
@[ext]
theorem
derivation.lift_kaehler_differential_unique
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M]
(f f' : Ω[S⁄R] →ₗ[S] M)
(hf : ⇑(f.comp_der) (kaehler_differential.D R S) = ⇑(f'.comp_der) (kaehler_differential.D R S)) :
f = f'
theorem
kaehler_differential.D_tensor_product_to
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
(x : ↥(kaehler_differential.ideal R S)) :
⇑((kaehler_differential.D R S).tensor_product_to) ↑x = ⇑((kaehler_differential.ideal R S).to_cotangent) x
def
kaehler_differential.linear_map_equiv_derivation
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
{M : Type u_3}
[add_comm_group M]
[module R M]
[module S M]
[is_scalar_tower R S M] :
The S-linear maps from Ω[S⁄R] to M are (S-linearly) equivalent to R-derivations
from S to M.
Equations
- kaehler_differential.linear_map_equiv_derivation R S = {to_fun := (⇑(derivation.llcomp.flip) (kaehler_differential.D R S)).to_fun, map_add' := _, map_smul' := _, inv_fun := derivation.lift_kaehler_differential _inst_7, left_inv := _, right_inv := _}
def
kaehler_differential.quotient_cotangent_ideal_ring_equiv
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
(tensor_product R S S ⧸ kaehler_differential.ideal R S ^ 2) ⧸ (kaehler_differential.ideal R S).cotangent_ideal ≃+* S
The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S.
def
kaehler_differential.quotient_cotangent_ideal
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
((tensor_product R S S ⧸ kaehler_differential.ideal R S ^ 2) ⧸ (kaehler_differential.ideal R S).cotangent_ideal) ≃ₐ[S] S
The quotient ring of S ⊗ S ⧸ J ^ 2 by Ω[S⁄R] is isomorphic to S as an S-algebra.
Equations
- kaehler_differential.quotient_cotangent_ideal R S = {to_fun := (kaehler_differential.quotient_cotangent_ideal_ring_equiv R S).to_fun, inv_fun := (kaehler_differential.quotient_cotangent_ideal_ring_equiv R S).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
theorem
kaehler_differential.End_equiv_aux
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(f : S →ₐ[R] tensor_product R S S ⧸ kaehler_differential.ideal R S ^ 2) :
(ideal.quotient.mkₐ R (kaehler_differential.ideal R S).cotangent_ideal).comp f = is_scalar_tower.to_alg_hom R S ((tensor_product R S S ⧸ kaehler_differential.ideal R S ^ 2) ⧸ (kaehler_differential.ideal R S).cotangent_ideal) ↔ (algebra.tensor_product.lmul' R).ker_square_lift.comp f = alg_hom.id R S
noncomputable
def
kaehler_differential.End_equiv_derivation'
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
derivation R S Ω[S⁄R] ≃ₗ[R] derivation R S ↥((kaehler_differential.ideal R S).cotangent_ideal)
Derivations into Ω[S⁄R] is equivalent to derivations
into (kaehler_differential.ideal R S).cotangent_ideal
def
kaehler_differential.End_equiv_aux_equiv
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
{f // (ideal.quotient.mkₐ R (kaehler_differential.ideal R S).cotangent_ideal).comp f = is_scalar_tower.to_alg_hom R S ((tensor_product R S S ⧸ kaehler_differential.ideal R S ^ 2) ⧸ (kaehler_differential.ideal R S).cotangent_ideal)} ≃ {f // (algebra.tensor_product.lmul' R).ker_square_lift.comp f = alg_hom.id R S}
(Implementation) An equiv version of kaehler_differential.End_equiv_aux.
Used in kaehler_differential.End_equiv.
Equations
- kaehler_differential.End_equiv_aux_equiv R S = (equiv.refl (S →ₐ[R] tensor_product R S S ⧸ kaehler_differential.ideal R S ^ 2)).subtype_equiv _
noncomputable
def
kaehler_differential.End_equiv
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
module.End S Ω[S⁄R] ≃ {f // (algebra.tensor_product.lmul' R).ker_square_lift.comp f = alg_hom.id R S}
The endomorphisms of Ω[S⁄R] corresponds to sections of the surjection S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S,
with J being the kernel of the multiplication map S ⊗[R] S →ₐ[R] S.
Equations
- kaehler_differential.End_equiv R S = (kaehler_differential.linear_map_equiv_derivation R S).to_equiv.trans ((kaehler_differential.End_equiv_derivation' R S).to_equiv.trans ((derivation_to_square_zero_equiv_lift (kaehler_differential.ideal R S).cotangent_ideal _).trans (kaehler_differential.End_equiv_aux_equiv R S)))
noncomputable
def
kaehler_differential.ker_total
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
The S-submodule of S →₀ S (the direct sum of copies of S indexed by S) generated by
the relations:
dx + dy = d(x + y)x dy + y dx = d(x * y)dr = 0forr ∈ Rwheredbis the unit in the copy ofSwith indexb.
This is the kernel of the surjection finsupp.total S Ω[S⁄R] S (kaehler_differential.D R S).
See kaehler_differential.ker_total_eq and kaehler_differential.total_surjective.
Equations
- kaehler_differential.ker_total R S = submodule.span S (set.range (λ (x : S × S), finsupp.single x.fst 1 + finsupp.single x.snd 1 - finsupp.single (x.fst + x.snd) 1) ∪ set.range (λ (x : S × S), finsupp.single x.snd x.fst + finsupp.single x.fst x.snd - finsupp.single (x.fst * x.snd) 1) ∪ set.range (λ (x : R), finsupp.single (⇑(algebra_map R S) x) 1))
theorem
kaehler_differential.ker_total_mkq_single_add
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(x y z : S) :
⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single (x + y) z) = ⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single x z) + ⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single y z)
theorem
kaehler_differential.ker_total_mkq_single_mul
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(x y z : S) :
⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single (x * y) z) = ⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single y (z * x)) + ⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single x (z * y))
theorem
kaehler_differential.ker_total_mkq_single_algebra_map
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(x : R)
(y : S) :
⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single (⇑(algebra_map R S) x) y) = 0
theorem
kaehler_differential.ker_total_mkq_single_algebra_map_one
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(x : S) :
⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single 1 x) = 0
theorem
kaehler_differential.ker_total_mkq_single_smul
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(r : R)
(x y : S) :
⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single (r • x) y) = r • ⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single x y)
noncomputable
def
kaehler_differential.derivation_quot_ker_total
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
derivation R S ((S →₀ S) ⧸ kaehler_differential.ker_total R S)
The (universal) derivation into (S →₀ S) ⧸ kaehler_differential.ker_total R S.
Equations
- kaehler_differential.derivation_quot_ker_total R S = {to_linear_map := {to_fun := λ (x : S), ⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single x 1), map_add' := _, map_smul' := _}, map_one_eq_zero' := _, leibniz' := _}
theorem
kaehler_differential.derivation_quot_ker_total_apply
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(x : S) :
⇑(kaehler_differential.derivation_quot_ker_total R S) x = ⇑((kaehler_differential.ker_total R S).mkq) (finsupp.single x 1)
theorem
kaehler_differential.ker_total_eq
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
linear_map.ker (finsupp.total S Ω[S⁄R] S ⇑(kaehler_differential.D R S)) = kaehler_differential.ker_total R S
theorem
kaehler_differential.total_surjective
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
function.surjective ⇑(finsupp.total S Ω[S⁄R] S ⇑(kaehler_differential.D R S))
@[simp]
theorem
kaehler_differential.quot_ker_total_equiv_apply
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(ᾰ : (S →₀ S) ⧸ kaehler_differential.ker_total R S) :
⇑(kaehler_differential.quot_ker_total_equiv R S) ᾰ = ((kaehler_differential.ker_total R S).liftq (finsupp.total S Ω[S⁄R] S ⇑(kaehler_differential.D R S)) _).to_fun ᾰ
noncomputable
def
kaehler_differential.quot_ker_total_equiv
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S] :
Ω[S⁄R] is isomorphic to S copies of S with kernel kaehler_differential.ker_total.
Equations
- kaehler_differential.quot_ker_total_equiv R S = {to_fun := ((kaehler_differential.ker_total R S).liftq (finsupp.total S Ω[S⁄R] S ⇑(kaehler_differential.D R S)) _).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑((kaehler_differential.derivation_quot_ker_total R S).lift_kaehler_differential), left_inv := _, right_inv := _}
theorem
kaehler_differential.ker_total_map
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(A : Type u_4)
(B : Type u_5)
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra S B]
[algebra R B]
[algebra A B]
[is_scalar_tower R S B]
[is_scalar_tower R A B]
(h : function.surjective ⇑(algebra_map A B)) :
submodule.map ((finsupp.map_range.linear_map (algebra.linear_map A B)).comp (finsupp.lmap_domain A A ⇑(algebra_map A B))) (kaehler_differential.ker_total R A) ⊔ submodule.span A (set.range (λ (x : S), finsupp.single (⇑(algebra_map S B) x) 1)) = submodule.restrict_scalars A (kaehler_differential.ker_total S B)
def
derivation.comp_algebra_map
{R : Type u_1}
[comm_ring R]
{M : Type u_3}
[add_comm_group M]
[module R M]
(A : Type u_4)
{B : Type u_5}
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
[algebra A B]
[is_scalar_tower R A B]
[module A M]
[module B M]
[is_scalar_tower A B M]
(d : derivation R B M) :
derivation R A M
For a tower R → A → B and an R-derivation B → M, we may compose with A → B to obtain an
R-derivation A → M.
Equations
- derivation.comp_algebra_map A d = {to_linear_map := d.to_linear_map.comp (is_scalar_tower.to_alg_hom R A B).to_linear_map, map_one_eq_zero' := _, leibniz' := _}
def
kaehler_differential.map
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(A : Type u_4)
(B : Type u_5)
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
[algebra A B]
[algebra S B]
[is_scalar_tower R A B]
[is_scalar_tower R S B]
[smul_comm_class S A B] :
The map Ω[A⁄R] →ₗ[A] Ω[B⁄R] given a square
A --→ B
↑ ↑
| |
R --→ S
Equations
theorem
kaehler_differential.map_comp_der
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(A : Type u_4)
(B : Type u_5)
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
[algebra A B]
[algebra S B]
[is_scalar_tower R A B]
[is_scalar_tower R S B]
[smul_comm_class S A B] :
⇑((kaehler_differential.map R S A B).comp_der) (kaehler_differential.D R A) = derivation.comp_algebra_map A (derivation.restrict_scalars R (kaehler_differential.D S B))
theorem
kaehler_differential.map_D
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(A : Type u_4)
(B : Type u_5)
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
[algebra A B]
[algebra S B]
[is_scalar_tower R A B]
[is_scalar_tower R S B]
[smul_comm_class S A B]
(x : A) :
⇑(kaehler_differential.map R S A B) (⇑(kaehler_differential.D R A) x) = ⇑(kaehler_differential.D S B) (⇑(algebra_map A B) x)
theorem
kaehler_differential.map_surjective_of_surjective
(R : Type u_1)
(S : Type u_2)
[comm_ring R]
[comm_ring S]
[algebra R S]
(A : Type u_4)
(B : Type u_5)
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
[algebra A B]
[algebra S B]
[is_scalar_tower R A B]
[is_scalar_tower R S B]
[smul_comm_class S A B]
(h : function.surjective ⇑(algebra_map A B)) :
function.surjective ⇑(kaehler_differential.map R S A B)
noncomputable
def
kaehler_differential.map_base_change
(R : Type u_1)
[comm_ring R]
(A : Type u_4)
(B : Type u_5)
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
[algebra A B]
[is_scalar_tower R A B] :
The lift of the map Ω[A⁄R] →ₗ[A] Ω[B⁄R] to the base change along A → B.
This is the first map in the exact sequence B ⊗[A] Ω[A⁄R] → Ω[B⁄R] → Ω[B⁄A] → 0.
Equations
- kaehler_differential.map_base_change R A B = _.lift (kaehler_differential.map R R A B)
@[simp]
theorem
kaehler_differential.map_base_change_tmul
(R : Type u_1)
[comm_ring R]
(A : Type u_4)
(B : Type u_5)
[comm_ring A]
[comm_ring B]
[algebra R A]
[algebra R B]
[algebra A B]
[is_scalar_tower R A B]
(x : B)
(y : Ω[A⁄R]) :
⇑(kaehler_differential.map_base_change R A B) (x ⊗ₜ[A] y) = x • ⇑(kaehler_differential.map R R A B) y