Module

RightDomain.lean

Nyll.EtaleFundamentalGroups.Kummer.Completions.ChosenFactor.RightDomain

2 declarations indexed from sourceView source ↗

Module documentation

Domain structure on the right coordinate of a chosen tensor factor

A chosen-factor equivalence B tensor[A] C = D embeds its right coordinate C into D whenever C/A is flat and B/A is faithful. Consequently a domain structure on the actual chosen factor pulls back to C. This avoids using Noetherianity of the complete two-dimensional base merely to prove that its explicit finite residue lift is a domain.

Imports2

Mathlib.RingTheory.Flat.Basic
Nyll.EtaleFundamentalGroups.Completions.FiniteEtale.ChosenFactorCoordinates

Imported by3

theorem

tensorChosenFactorRight_algebraMap_injective

L30 ↗

EtaleFundamentalGroups.Kummer.tensorChosenFactorRight_algebraMap_injective

Documentation

The transported right-coordinate map of a chosen tensor factor is injective.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
universe uA uB uC uD

Lean source · full declaration

theorem tensorChosenFactorRight_algebraMap_injective
    {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD}
    [CommRing A] [CommRing B] [CommRing C] [CommRing D]
    [Algebra A B] [Algebra A C] [Algebra B D]
    [FaithfulSMul A B] [Module.Flat A C]
    (e : (B ⊗[A] C) ≃ₐ[B] D) :
    letI : Algebra C D :=
      (e.toRingEquiv.toRingHom.comp
        (Algebra.TensorProduct.includeRight : C →ₐ[A] B ⊗[A] C).toRingHom).toAlgebra
    Function.Injective (algebraMap C D) := by
  let : Algebra C D :=
    (e.toRingEquiv.toRingHom.comp
      (Algebra.TensorProduct.includeRight : C →ₐ[A] B ⊗[A] C).toRingHom).toAlgebra
  change Function.Injective
    (e.toRingEquiv.toRingHom.comp
      (Algebra.TensorProduct.includeRight : C →ₐ[A] B ⊗[A] C).toRingHom)
  exact e.injective.comp <|
    Algebra.TensorProduct.includeRight_injective
      (FaithfulSMul.algebraMap_injective A B)

theorem

tensorChosenFactorRight_isDomain

L52 ↗

EtaleFundamentalGroups.Kummer.tensorChosenFactorRight_isDomain