Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-03 23:08 73f96237

View on Github →

chore(ring_theory/kaehler): extract from ring_theory/derivation (#18935) This section of the file needs heavier imports than the first half; and this splits the content nicely in two. The lemmas are moved without modification. One very minor docstring typo is fixed.

Estimated changes

Modified src/ring_theory/derivation.lean

deleted def derivation.comp_algebra_map

deleted def derivation.lift_kaehler_differential

deleted theorem derivation.lift_kaehler_differential_D

deleted theorem derivation.lift_kaehler_differential_apply

deleted theorem derivation.lift_kaehler_differential_comp

deleted theorem derivation.lift_kaehler_differential_comp_D

deleted theorem derivation.lift_kaehler_differential_unique

deleted def derivation.tensor_product_to

deleted theorem derivation.tensor_product_to_mul

deleted theorem derivation.tensor_product_to_tmul

deleted def kaehler_differential.D

deleted theorem kaehler_differential.D_apply

deleted def kaehler_differential.D_linear_map

deleted theorem kaehler_differential.D_linear_map_apply

deleted theorem kaehler_differential.D_tensor_product_to

deleted def kaehler_differential.End_equiv

deleted theorem kaehler_differential.End_equiv_aux

deleted def kaehler_differential.End_equiv_aux_equiv

deleted def kaehler_differential.End_equiv_derivation'

deleted def kaehler_differential.derivation_quot_ker_total

deleted theorem kaehler_differential.derivation_quot_ker_total_apply

deleted theorem kaehler_differential.derivation_quot_ker_total_lift_comp_total

deleted def kaehler_differential.from_ideal

deleted def kaehler_differential.ideal

deleted def kaehler_differential.ker_total

deleted theorem kaehler_differential.ker_total_eq

deleted theorem kaehler_differential.ker_total_map

deleted theorem kaehler_differential.ker_total_mkq_single_add

deleted theorem kaehler_differential.ker_total_mkq_single_algebra_map

deleted theorem kaehler_differential.ker_total_mkq_single_algebra_map_one

deleted theorem kaehler_differential.ker_total_mkq_single_mul

deleted theorem kaehler_differential.ker_total_mkq_single_smul

deleted def kaehler_differential.linear_map_equiv_derivation

deleted def kaehler_differential.map

deleted theorem kaehler_differential.map_D

deleted def kaehler_differential.map_base_change

deleted theorem kaehler_differential.map_base_change_tmul

deleted theorem kaehler_differential.map_comp_der

deleted theorem kaehler_differential.map_surjective_of_surjective

deleted theorem kaehler_differential.one_smul_sub_smul_one_mem_ideal

deleted def kaehler_differential.quot_ker_total_equiv

deleted theorem kaehler_differential.quot_ker_total_equiv_symm_comp_D

deleted def kaehler_differential.quotient_cotangent_ideal

deleted def kaehler_differential.quotient_cotangent_ideal_ring_equiv

deleted theorem kaehler_differential.span_range_derivation

deleted theorem kaehler_differential.span_range_eq_ideal

deleted theorem kaehler_differential.submodule_span_range_eq_ideal

deleted theorem kaehler_differential.tensor_product_to_surjective

deleted theorem kaehler_differential.total_surjective

deleted def kaehler_differential

Modified src/ring_theory/etale.lean

Created src/ring_theory/kaehler.lean

added def derivation.comp_algebra_map

added def derivation.lift_kaehler_differential

added theorem derivation.lift_kaehler_differential_D

added theorem derivation.lift_kaehler_differential_apply

added theorem derivation.lift_kaehler_differential_comp

added theorem derivation.lift_kaehler_differential_comp_D

added theorem derivation.lift_kaehler_differential_unique

added def derivation.tensor_product_to

added theorem derivation.tensor_product_to_mul

added theorem derivation.tensor_product_to_tmul

added def kaehler_differential.D

added theorem kaehler_differential.D_apply

added def kaehler_differential.D_linear_map

added theorem kaehler_differential.D_linear_map_apply

added theorem kaehler_differential.D_tensor_product_to

added def kaehler_differential.End_equiv

added theorem kaehler_differential.End_equiv_aux

added def kaehler_differential.End_equiv_aux_equiv

added def kaehler_differential.End_equiv_derivation'

added def kaehler_differential.derivation_quot_ker_total

added theorem kaehler_differential.derivation_quot_ker_total_apply

added theorem kaehler_differential.derivation_quot_ker_total_lift_comp_total

added def kaehler_differential.from_ideal

added def kaehler_differential.ideal

added def kaehler_differential.ker_total

added theorem kaehler_differential.ker_total_eq

added theorem kaehler_differential.ker_total_map

added theorem kaehler_differential.ker_total_mkq_single_add

added theorem kaehler_differential.ker_total_mkq_single_algebra_map

added theorem kaehler_differential.ker_total_mkq_single_algebra_map_one

added theorem kaehler_differential.ker_total_mkq_single_mul

added theorem kaehler_differential.ker_total_mkq_single_smul

added def kaehler_differential.linear_map_equiv_derivation

added def kaehler_differential.map

added theorem kaehler_differential.map_D

added def kaehler_differential.map_base_change

added theorem kaehler_differential.map_base_change_tmul

added theorem kaehler_differential.map_comp_der

added theorem kaehler_differential.map_surjective_of_surjective

added theorem kaehler_differential.one_smul_sub_smul_one_mem_ideal

added def kaehler_differential.quot_ker_total_equiv

added theorem kaehler_differential.quot_ker_total_equiv_symm_comp_D

added def kaehler_differential.quotient_cotangent_ideal

added def kaehler_differential.quotient_cotangent_ideal_ring_equiv

added theorem kaehler_differential.span_range_derivation

added theorem kaehler_differential.span_range_eq_ideal

added theorem kaehler_differential.submodule_span_range_eq_ideal

added theorem kaehler_differential.tensor_product_to_surjective

added theorem kaehler_differential.total_surjective

added def kaehler_differential